---

Step * of Lemma lconnects_wf

∀[p:IdLnk List]. ∀[i,j:Id].  (lconnects(p;i;j) ∈ ℙ)
BY
{ (Unfold `lconnects` 0 THEN Auto') }

---

Latex:


\mforall{}[p:IdLnk  List].  \mforall{}[i,j:Id].    (lconnects(p;i;j)  \mmember{}  \mBbbP{})


By

(Unfold  `lconnects`  0  THEN  Auto')

---

Home Index