---

Step * of Lemma strict-majority-or-first_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:{L:T List| ||L|| ≥ 1 } ].  (strict-majority-or-first(eq;L) ∈ T)
BY
{ TACTIC:ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:\{L:T  List|  ||L||  \mgeq{}  1  \}  ].    (strict-majority-or-first(eq;L)  \mmember{}  T)


By

---

Latex:
TACTIC:ProveWfLemma

---

Home Index