Nuprl Lemma : ycomb_wf_trivial
Y ∈ Void ⟶ Void
Proof
Definitions occuring in Statement :
ycomb: Y,
member: t ∈ T,
function: x:A ⟶ B[x],
void: Void
Definitions unfolded in proof :
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
functionExtensionality,
voidElimination,
voidEquality
Latex:
Y \mmember{} Void {}\mrightarrow{} Void
Date html generated:
2019_06_20-AM-11_19_40
Last ObjectModification:
2018_12_07-PM-02_14_20
Theory : sqequal_1
Home
Index