Nuprl Lemma : decidable__equal_IdLnk
∀a,b:IdLnk. Dec(a = b ∈ IdLnk)
Proof
Definitions occuring in Statement :
IdLnk: IdLnk,
decidable: Dec(P),
all: ∀x:A. B[x],
equal: s = t ∈ T
Lemmas :
decidable__assert,
eq_lnk_wf,
IdLnk_wf,
equal_wf,
assert_wf,
all_wf,
decidable_wf
\mforall{}a,b:IdLnk. Dec(a = b)
Date html generated:
2015_07_17-AM-09_12_55
Last ObjectModification:
2015_01_28-AM-07_55_56
Home
Index