---

Step * of Lemma remove-repeats-fun-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 RepUR ``remove-repeats-fun`` 0
   THEN Try (Complete (Auto))
   THEN Try (Fold `remove-repeats-fun` 0)
   THEN (EqCD THEN Auto)
   THEN (RWO "-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  RepUR  ``remove-repeats-fun``  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Fold  `remove-repeats-fun`  0)
  THEN  (EqCD  THEN  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (RWO  "filter-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index