---

Step * of Lemma thread-name_wf

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

---

Latex:


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


By

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

---

Home Index