---

Step * of Lemma mk_lnk_wf

∀[i,j,n:Id].  ((link(n) from i to j) ∈ IdLnk)
BY
{ (Unfolds ``mk_lnk IdLnk`` 0 THEN Auto) }

---

Latex:


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


By

(Unfolds  ``mk\_lnk  IdLnk``  0  THEN  Auto)

---

Home Index