---

Step * of Lemma count-all

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  count(P;L) ~ ||L|| supposing (∀x∈L.↑(P x))
BY
{ (Auto THEN (RWO "count-as-filter" 0 THENA Auto) THEN RWO "filter_trivial" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    count(P;L)  \msim{}  ||L||  supposing  (\mforall{}x\mmember{}L.\muparrow{}(P  x))


By

---

Latex:
(Auto  THEN  (RWO  "count-as-filter"  0  THENA  Auto)  THEN  RWO  "filter\_trivial"  0  THEN  Auto)

---

Home Index