---

Step * of Lemma kind-loc_wf

∀[k:Knd]. ∀[i:Id].  (kind-loc(k;i) ∈ 𝔹)
BY
{ (Auto THEN (D (-2)) THEN RepUR ``kind-loc islocal lnk`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  \mforall{}[i:Id].    (kind-loc(k;i)  \mmember{}  \mBbbB{})


By

(Auto  THEN  (D  (-2))  THEN  RepUR  ``kind-loc  islocal  lnk``  0  THEN  Auto)

---

Home Index