---

{ maname-deq()  EqDecider(MaName) }

{ Proof }

---

Definitions occuring in Statement :  maname-deq: maname-deq(),  MaName: MaName,  member: t  T,  deq: EqDecider(T)
Definitions :  member: t  T,  MaName: MaName,  maname-deq: maname-deq(),  all: x:A. B[x]
Lemmas :  union-deq_wf,  LocKnd_wf,  Id_wf,  locknd-deq_wf,  product-deq_wf,  id-deq_wf

---

maname-deq()  \mmember{}  EqDecider(MaName)


Date html generated: 2010_08_26-PM-11_42_42
Last ObjectModification: 2009_03_22-PM-01_23_59

Home Index