---

{ [t:Thread]. (t.session  Id) }

{ Proof }

---

Definitions occuring in Statement :  thread-session: t.session,  thread: Thread,  Id: Id,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  thread: Thread,  member: t  T,  thread-session: t.session,  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  pi2_wf,  Id_wf

---

\mforall{}[t:Thread].  (t.session  \mmember{}  Id)


Date html generated: 2011_08_16-AM-11_10_36
Last ObjectModification: 2011_06_20-AM-00_18_42

Home Index