---

Step * of Lemma lg-map_wf

∀[T,S:Type]. ∀[f:T ⟶ S]. ∀[g:LabeledGraph(T)].  (lg-map(f;g) ∈ LabeledGraph(S))
BY
{ (Auto THEN D -1 THEN Unfold `labeled-graph` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[f:T  {}\mrightarrow{}  S].  \mforall{}[g:LabeledGraph(T)].    (lg-map(f;g)  \mmember{}  LabeledGraph(S))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Unfold  `labeled-graph`  0  THEN  ProveWfLemma)

---

Home Index