---

Step * of Lemma filter-commutes

∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List].  (filter(P1;filter(P2;L)) ~ filter(P2;filter(P1;L)))
BY
{ ObviousListInduction }

---

Latex:

---

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


By

---

Latex:
ObviousListInduction

---

Home Index