---

Step * of Lemma make-lg_wf

∀[T:Type]. ∀[L:T List].  (make-lg(L) ∈ LabeledGraph(T))
BY
{ (Unfolds ``labeled-graph make-lg`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    (make-lg(L)  \mmember{}  LabeledGraph(T))


By

---

Latex:
(Unfolds  ``labeled-graph  make-lg``  0  THEN  Auto)

---

Home Index