---

Step * of Lemma filter_filter_reduce

∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List].
  filter(P1;filter(P2;L)) ~ filter(P1;L) supposing ∀x:T. ((↑(P1 x)) ⇒ (↑(P2 x)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN Try ((EqCD THEN Try (BackThruSomeHyp) THEN Auto))) }

1
1. T : Type
2. P1 : T ⟶ 𝔹
3. P2 : T ⟶ 𝔹
4. u : T
5. ¬↑(P2 u)
6. v : T List
7. filter(P1;filter(P2;v)) ~ filter(P1;v) supposing ∀x:T. ((↑(P1 x)) ⇒ (↑(P2 x)))
8. ↑(P1 u)
9. ∀x:T. ((↑(P1 x)) ⇒ (↑(P2 x)))
⊢ filter(P1;filter(P2;v)) ~ [u / filter(P1;v)]

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((EqCD  THEN  Try  (BackThruSomeHyp)  THEN  Auto)))

---

Home Index