Step * of Lemma strict-majority-or-first_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:{L:T List| ||L|| ≥ ].  (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