Nuprl Lemma : assert_of_tt
↑tt
Proof
Definitions occuring in Statement :
assert: ↑b,
btrue: tt
Definitions unfolded in proof :
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
natural_numberEquality
Latex:
\muparrow{}tt
Date html generated:
2016_05_13-PM-03_20_36
Last ObjectModification:
2015_12_26-AM-09_10_52
Theory : union
Home
Index