Nuprl Lemma : is_list_axiom_lemma
is-list(Ax) ~ tt
Proof
Definitions occuring in Statement :
is-list: is-list(t),
btrue: tt,
sqequal: s ~ t,
axiom: Ax
Definitions unfolded in proof :
is-list: is-list(t)
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity
Latex:
is-list(Ax) \msim{} tt
Date html generated:
2016_05_15-PM-10_07_33
Last ObjectModification:
2015_12_27-PM-06_00_42
Theory : eval!all
Home
Index