---

Step * of Lemma hasloc_wf

∀[i:Id]. ∀[k:Knd].  (hasloc(k;i) ∈ 𝔹)
BY
{ (Auto THEN Unfold `hasloc` 0 THEN AutoBoolCase ⌜isrcv(k)⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[i:Id].  \mforall{}[k:Knd].    (hasloc(k;i)  \mmember{}  \mBbbB{})


By

---

Latex:
(Auto  THEN  Unfold  `hasloc`  0  THEN  AutoBoolCase  \mkleeneopen{}isrcv(k)\mkleeneclose{}\mcdot{})

---

Home Index