---

Step * of Lemma islocal-implies

∀[k:Knd]. locl(act(k)) = k ∈ Knd supposing ↑islocal(k)
BY
{ ((D 0 THENA Auto) THEN KindCases THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  KindCases  THEN  Auto)

---

Home Index