---

Step * of Lemma thread-session_wf

∀[t:Thread]. (t.session ∈ Id)
BY
{ (Unfolds ``thread thread-session`` 0 THEN Auto) }

---

Latex:


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


By

(Unfolds  ``thread  thread-session``  0  THEN  Auto)

---

Home Index