---

{ [a:Atom1]. [k:Knd].  k:Knd||a }

{ Proof }

---

Definitions occuring in Statement :  Knd: Knd,  uall: [x:A]. B[x],  free-from-atom: x:T||a,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  Knd: Knd,  member: t  T
Lemmas :  IdLnk_wf,  Id_wf,  free-from-atom-Id,  free-from-atom-IdLnk

---

\mforall{}[a:Atom1].  \mforall{}[k:Knd].    k:Knd||a


Date html generated: 2011_08_10-AM-07_45_31
Last ObjectModification: 2011_06_18-AM-08_10_23

Home Index