{ [a:Id]. (locl(a)  Knd) }

{ Proof }



Definitions occuring in Statement :  locl: locl(a) Knd: Knd Id: Id uall: [x:A]. B[x] member: t  T
Definitions :  uall: [x:A]. B[x] member: t  T Knd: Knd locl: locl(a)
Lemmas :  IdLnk_wf Id_wf

\mforall{}[a:Id].  (locl(a)  \mmember{}  Knd)


Date html generated: 2011_08_10-AM-07_45_40
Last ObjectModification: 2011_06_18-AM-08_10_31

Home Index