---

Step * of Lemma tagof_wf

∀[k:Knd]. tag(k) ∈ Id supposing ↑isrcv(k)
BY
{ (Unfolds ``Knd isrcv tagof`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  tag(k)  \mmember{}  Id  supposing  \muparrow{}isrcv(k)


By

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

---

Home Index