Nuprl Lemma : church_null_nil_lemma
church-null() church-nil() ~ church-true()
Proof
Definitions occuring in Statement :
church-null: church-null(),
church-nil: church-nil(),
church-true: church-true(),
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
church-null: church-null(),
church-nil: church-nil()
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity
Latex:
church-null() church-nil() \msim{} church-true()
Date html generated:
2016_05_15-PM-03_22_48
Last ObjectModification:
2015_12_27-PM-01_05_12
Theory : general
Home
Index