---

Step * of Lemma min_w_unit_l_tree_wf

∀[T:Type]. ∀[u1,u2:T?]. ∀[f:T ⟶ ℤ].  (min_w_unit_l_tree(u1;u2;f) ∈ T?)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[u1,u2:T?].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (min\_w\_unit\_l\_tree(u1;u2;f)  \mmember{}  T?)


By

---

Latex:
ProveWfLemma

---

Home Index