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: 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