---

{ IdLnkDeq  EqDecider(IdLnk) }

{ Proof }

---

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

---

IdLnkDeq  \mmember{}  EqDecider(IdLnk)


Date html generated: 2010_08_26-PM-11_35_14
Last ObjectModification: 2008_02_27-PM-09_31_58

Home Index