---

Step * of Lemma remove-repeats-filter

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].
  (remove-repeats(eq;filter(P;L)) = filter(P;remove-repeats(eq;L)) ∈ (T List))
BY
{ ((InductionOnList THEN Reduce 0)
   THEN Auto
   THEN AutoSplit
   THEN Try ((EqCD THEN Auto))
   THEN (RWW "-1 -2 filter-filter" 0 THENA Auto)
   THEN (EqCD
         THEN Auto
         THEN Reduce 0
         THEN Ext
         THEN Reduce 0
         THEN Auto
         THEN AutoBoolCase ⌜P x⌝⋅
         THEN AutoBoolCase ⌜eq x u⌝⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (remove-repeats(eq;filter(P;L))  =  filter(P;remove-repeats(eq;L)))


By

---

Latex:
((InductionOnList  THEN  Reduce  0)
  THEN  Auto
  THEN  AutoSplit
  THEN  Try  ((EqCD  THEN  Auto))
  THEN  (RWW  "-1  -2  filter-filter"  0  THENA  Auto)
  THEN  (EqCD
              THEN  Auto
              THEN  Reduce  0
              THEN  Ext
              THEN  Reduce  0
              THEN  Auto
              THEN  AutoBoolCase  \mkleeneopen{}P  x\mkleeneclose{}\mcdot{}
              THEN  AutoBoolCase  \mkleeneopen{}eq  x  u\mkleeneclose{}\mcdot{})\mcdot{})

---

Home Index