Nuprl Lemma : church-zero_wf2
cZ ∈ INat
Proof
Definitions occuring in Statement :
indNat: INat,
church-zero: cZ,
member: t ∈ T
Definitions unfolded in proof :
indNat: INat,
member: t ∈ T
Lemmas referenced :
church-zero_wf,
church-iZ
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependentIntersection_memberEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
cZ \mmember{} INat
Date html generated:
2020_05_20-AM-08_05_51
Last ObjectModification:
2019_11_15-PM-10_42_12
Theory : general
Home
Index