---

Step * of Lemma vlnk_wf

∀[i,j,x:Id].  (link_x from i to j ∈ IdLnk)
BY
{ (Unfolds ``IdLnk vlnk`` 0 THEN Auto) }

---

Latex:


\mforall{}[i,j,x:Id].    (link\_x  from  i  to  j  \mmember{}  IdLnk)


By

(Unfolds  ``IdLnk  vlnk``  0  THEN  Auto)

---

Home Index