---

Step * of Lemma rcvs-on_wf

∀[tg:Id]. ∀[links:IdLnk List].  (Rcvs(tg) on links ∈ {k:Knd| ↑isrcv(k)}  List)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[tg:Id].  \mforall{}[links:IdLnk  List].    (Rcvs(tg)  on  links  \mmember{}  \{k:Knd|  \muparrow{}isrcv(k)\}    List)


By

ProveWfLemma

---

Home Index