Nuprl Lemma : decidable__equal_MaName
∀x,y:MaName. Dec(x = y ∈ MaName)
Proof
Definitions occuring in Statement :
MaName: MaName,
decidable: Dec(P),
all: ∀x:A. B[x],
equal: s = t ∈ T
Lemmas :
equal_wf,
MaName_wf,
assert_wf,
maname-deq_wf,
deq_wf,
decidable__assert,
decidable_functionality,
iff_weakening_uiff
\mforall{}x,y:MaName. Dec(x = y)
Date html generated:
2015_07_17-AM-09_14_54
Last ObjectModification:
2015_01_28-AM-07_54_05
Home
Index