---

Step * of Lemma lg-append-contains

∀[T:Type]. ∀g1,g2:LabeledGraph(T).  (g1 ⊆ lg-append(g1;g2) ∧ g2 ⊆ lg-append(g1;g2))
BY
{ (Auto THEN Unfold `lg-contains` 0) }

1
1. [T] : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
⊢ ∃ga,gb:LabeledGraph(T). (lg-append(g1;g2) = lg-append(ga;lg-append(g1;gb)) ∈ LabeledGraph(T))

2
1. [T] : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
4. g1 ⊆ lg-append(g1;g2)
⊢ ∃ga,gb:LabeledGraph(T). (lg-append(g1;g2) = lg-append(ga;lg-append(g2;gb)) ∈ LabeledGraph(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}g1,g2:LabeledGraph(T).    (g1  \msubseteq{}  lg-append(g1;g2)  \mwedge{}  g2  \msubseteq{}  lg-append(g1;g2))


By

---

Latex:
(Auto  THEN  Unfold  `lg-contains`  0)

---

Home Index