---

{ es-LnkTag-deq  EqDecider(IdLnk  Id) }

{ Proof }

---

Definitions occuring in Statement :  es-LnkTag-deq: es-LnkTag-deq,  IdLnk: IdLnk,  Id: Id,  member: t  T,  product: x:A  B[x],  deq: EqDecider(T)
Definitions :  member: t  T,  es-LnkTag-deq: es-LnkTag-deq,  all: x:A. B[x]
Lemmas :  product-deq_wf,  IdLnk_wf,  Id_wf,  idlnk-deq_wf,  id-deq_wf

---

es-LnkTag-deq  \mmember{}  EqDecider(IdLnk  \mtimes{}  Id)


Date html generated: 2010_08_27-AM-01_08_24
Last ObjectModification: 2009_12_16-AM-12_38_30

Home Index