---

{ KindDeq  EqDecider(Knd) }

{ Proof }

---

Definitions occuring in Statement :  Kind-deq: KindDeq,  Knd: Knd,  member: t  T,  deq: EqDecider(T)
Definitions :  Kind-deq: KindDeq,  member: t  T,  Knd: Knd,  all: x:A. B[x]
Lemmas :  product-deq_wf,  IdLnk_wf,  idlnk-deq_wf,  Id_wf,  id-deq_wf,  union-deq_wf

---

KindDeq  \mmember{}  EqDecider(Knd)


Date html generated: 2010_08_26-PM-11_38_43
Last ObjectModification: 2008_02_27-PM-09_33_03

Home Index