---

Step * of Lemma max_w_unit_l_tree_wf

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

---

Latex:


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


By

ProveWfLemma

---

Home Index