---

{ [l:IdLnk]. (lname(l)  Id) }

{ Proof }

---

Definitions occuring in Statement :  lname: lname(l),  IdLnk: IdLnk,  Id: Id,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  IdLnk: IdLnk,  member: t  T,  lname: lname(l),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  pi2_wf,  Id_wf

---

\mforall{}[l:IdLnk].  (lname(l)  \mmember{}  Id)


Date html generated: 2011_08_10-AM-07_46_34
Last ObjectModification: 2011_06_18-AM-08_12_15

Home Index