---

Step * of Lemma strict-majority_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  (strict-majority(eq;L) ∈ T?)
BY
{ (Auto THEN Unfold `strict-majority` 0 THEN GenConclAtAddrType ⌜(T × ℤ) List⌝ [2;1]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].    (strict-majority(eq;L)  \mmember{}  T?)


By

---

Latex:
(Auto  THEN  Unfold  `strict-majority`  0  THEN  GenConclAtAddrType  \mkleeneopen{}(T  \mtimes{}  \mBbbZ{})  List\mkleeneclose{}  [2;1]\mcdot{}  THEN  Auto)

---

Home Index