---

Step * of Lemma remove-repeats-fun-as-remove-repeats-map

∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].
  (map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (Complete ((RepUR ``remove-repeats-fun`` 0 THEN Auto)))
   THEN Unfold `remove-repeats-fun` 0
   THEN Reduce 0
   THEN Fold `remove-repeats-fun` 0
   THEN (EqCD THEN Auto)
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN (RWO "filter-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:EqDecider(B)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[L:A  List].
    (map(f;remove-repeats-fun(eq;f;L))  =  remove-repeats(eq;map(f;L)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (Complete  ((RepUR  ``remove-repeats-fun``  0  THEN  Auto)))
  THEN  Unfold  `remove-repeats-fun`  0
  THEN  Reduce  0
  THEN  Fold  `remove-repeats-fun`  0
  THEN  (EqCD  THEN  Auto)
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  (RWO  "filter-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index