---

{ a,b:Knd.  Dec(a = b) }

{ Proof }

---

Definitions occuring in Statement :  Knd: Knd,  decidable: Dec(P),  all: x:A. B[x],  equal: s = t
Definitions :  all: x:A. B[x],  prop: ,  member: t  T
Lemmas :  decidable__assert,  eq_knd_wf,  assert_wf,  decidable_wf,  Knd_wf

---

\mforall{}a,b:Knd.    Dec(a  =  b)


Date html generated: 2010_08_26-PM-11_38_49
Last ObjectModification: 2009_03_12-PM-02_16_49

Home Index