---

Step * of Lemma lg-append-nil

∀[T:Type]. ∀[g:LabeledGraph(T)].  (lg-append(g;lg-nil()) = g ∈ LabeledGraph(T))
BY
{ (RepUR ``lg-append lg-nil`` 0 THEN Auto THEN RWO "append-nil" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].    (lg-append(g;lg-nil())  =  g)


By

---

Latex:
(RepUR  ``lg-append  lg-nil``  0  THEN  Auto  THEN  RWO  "append-nil"  0  THEN  Auto)

---

Home Index