---

Step * of Lemma lg-label2_wf

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)].  (lg-label2(g;x) ∈ T)
BY
{ (InstLemma `lg-label_wf` [] THEN Unfold `lg-label2` 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[x:\mBbbN{}lg-size(g)].    (lg-label2(g;x)  \mmember{}  T)


By

---

Latex:
(InstLemma  `lg-label\_wf`  []  THEN  Unfold  `lg-label2`  0  THEN  Trivial)

---

Home Index