---

Step * of Lemma filter-sq

∀[T:Type]. ∀[L:T List]. ∀[P,Q:{x:T| (x ∈ L)}  ⟶ 𝔹].
  filter(P;L) ~ filter(Q;L) supposing ∀x:{x:T| (x ∈ L)} . (↑(P x) ⇐⇒ ↑(Q x))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN Try (Trivial)
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Try ((D (-1) THEN BackThruSomeHyp THEN Complete (Auto)))
   THEN Try ((D (-2) THEN BackThruSomeHyp THEN Complete (Auto)))
   THEN Try ((EqCD THENL [Trivial; Id]))
   THEN RepeatFor 2 ((BackThruSomeHyp THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P,Q:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].
    filter(P;L)  \msim{}  filter(Q;L)  supposing  \mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  (\muparrow{}(P  x)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(Q  x))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Try  ((D  (-1)  THEN  BackThruSomeHyp  THEN  Complete  (Auto)))
  THEN  Try  ((D  (-2)  THEN  BackThruSomeHyp  THEN  Complete  (Auto)))
  THEN  Try  ((EqCD  THENL  [Trivial;  Id]))
  THEN  RepeatFor  2  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index