---

Step * of Lemma islocal_wf

∀[k:Knd]. (islocal(k) ∈ 𝔹)
BY
{ (Unfolds ``islocal Knd`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  (islocal(k)  \mmember{}  \mBbbB{})


By

(Unfolds  ``islocal  Knd``  0  THEN  Auto)

---

Home Index