---

Step * of Lemma map-filter-proof2

∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
  ∀[L:T List]. (map(f;filter(P;L)) ~ filter(Q;map(f;L))) supposing ∀x:T. Q (f x) = P x
BY
{ (Auto
   THEN (RWO "filter-map" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (InstHyp [⌜u⌝] (-4)⋅ THENA Auto)
   THEN HypSubst' (-1)0
   THEN RevHypSubst (-2) 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[Q:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[L:T  List].  (map(f;filter(P;L))  \msim{}  filter(Q;map(f;L)))  supposing  \mforall{}x:T.  Q  (f  x)  =  P  x


By

---

Latex:
(Auto
  THEN  (RWO  "filter-map"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)0
  THEN  RevHypSubst  (-2)  0
  THEN  Trivial)

---

Home Index