---

Step * of Lemma actof_wf

∀[k:Knd]. act(k) ∈ Id supposing ↑islocal(k)
BY
{ (Unfolds ``Knd islocal actof`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:Knd].  act(k)  \mmember{}  Id  supposing  \muparrow{}islocal(k)


By

---

Latex:
(Unfolds  ``Knd  islocal  actof``  0  THEN  Auto)

---

Home Index