Nuprl Lemma : eq_lnk_self
∀[l:IdLnk]. l = l = tt
Proof
Definitions occuring in Statement :
eq_lnk: a = b,
IdLnk: IdLnk,
btrue: tt,
bool: 𝔹,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
iff_imp_equal_bool,
eq_lnk_wf,
btrue_wf,
equal_wf,
IdLnk_wf,
true_wf,
assert-eq-lnk,
assert_wf,
iff_wf,
member_wf
\mforall{}[l:IdLnk]. l = l = tt
Date html generated:
2015_07_17-AM-09_12_56
Last ObjectModification:
2015_01_28-AM-07_56_18
Home
Index