---

Step * of Lemma count-length-filter

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].  (count(P;L) ~ ||filter(P;L)||)
BY
{ (Unfold `count` 0 THEN (InductionOnList THEN Reduce 0) THEN Auto{1,3}-1 THEN HypSubst' -1 0 THEN AutoSplit) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `count`  0
  THEN  (InductionOnList  THEN  Reduce  0)
  THEN  Auto\{1,3\}-1
  THEN  HypSubst'  -1  0
  THEN  AutoSplit)

---

Home Index