---

Step * of Lemma filter_filter

∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List].  (filter(P1;filter(P2;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P1,P2:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (filter(P1;filter(P2;L))  \msim{}  filter(\mlambda{}t.((P1  t)  \mwedge{}\msubb{}  (P2  t));L))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index