---

Step * of Lemma isrcvl_wf

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

---

Latex:


\mforall{}[k:Knd].  \mforall{}[l:IdLnk].    (isrcvl(l;k)  \mmember{}  \mBbbB{})


By

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

---

Home Index