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