---

Step * of Lemma lg-nil-append

∀[T:Type]. ∀[g:LabeledGraph(T)].  (lg-append(lg-nil();g) ~ g)
BY
{ (RepUR ``lg-append lg-nil lg-size`` 0 THEN (UnivCD THENA Auto)) }

1
1. T : Type
2. g : LabeledGraph(T)
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)>;g) ~ g

---

Latex:

---

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


By

---

Latex:
(RepUR  ``lg-append  lg-nil  lg-size``  0  THEN  (UnivCD  THENA  Auto))

---

Home Index