---

Step * of Lemma hasloc_wf

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

---

Latex:


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


By

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

---

Home Index