---

Step * of Lemma poss-maj_wf

∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T.  (poss-maj(eq;L;x) ∈ ℕ × T)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.    (poss-maj(eq;L;x)  \mmember{}  \mBbbN{}  \mtimes{}  T)


By

---

Latex:
ProveWfLemma

---

Home Index