---

{ x,y:MaName.  Dec(x = y) }

{ Proof }

---

Definitions occuring in Statement :  MaName: MaName,  decidable: Dec(P),  all: x:A. B[x],  equal: s = t
Definitions :  all: x:A. B[x],  member: t  T,  prop: ,  iff: P  Q,  rev_implies: P  Q,  implies: P  Q,  and: P  Q
Lemmas :  deq_property,  MaName_wf,  maname-deq_wf,  decidable_functionality,  assert_wf,  eqof_wf,  decidable__assert

---

\mforall{}x,y:MaName.    Dec(x  =  y)


Date html generated: 2010_08_26-PM-11_42_43
Last ObjectModification: 2009_03_22-PM-01_23_56

Home Index