---

Step * of Lemma min_w_ord_wf

∀[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ].  (min_w_ord(t1;t2;f) ∈ T)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[T:Type].  \mforall{}[t1,t2:T].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (min\_w\_ord(t1;t2;f)  \mmember{}  T)


By

ProveWfLemma

---

Home Index