---

Step * of Lemma count-as-filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  (count(P;L) ~ ||filter(P;L)||)
BY
{ (InductionOnList
   THEN RepUR ``count filter`` 0
   THEN Try (Trivial)
   THEN AutoSplit
   THEN Folds ``count filter`` 0
   THEN RWO "-1 -2" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``count  filter``  0
  THEN  Try  (Trivial)
  THEN  AutoSplit
  THEN  Folds  ``count  filter``  0
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index