---

Step * of Lemma isrcv_wf

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

---

Latex:


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


By

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

---

Home Index