---

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

{ Proof }

---

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

---

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


Date html generated: 2010_08_26-PM-11_35_19
Last ObjectModification: 2008_02_27-PM-09_32_20

Home Index