---

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

∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].
  (||remove-repeats-fun(eq;f;L)|| = ||remove-repeats(eq;map(f;L))|| ∈ ℤ)
BY
{ (Auto
   THEN (InstLemma `length-map` [⌜f⌝;⌜A⌝;⌜remove-repeats-fun(eq;f;L)⌝]⋅ THENA Auto)
   THEN RevHypSubst (-1) 0
   THEN RWO "remove-repeats-fun-as-remove-repeats-map" 0⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `length-map`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}remove-repeats-fun(eq;f;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst  (-1)  0
  THEN  RWO  "remove-repeats-fun-as-remove-repeats-map"  0\mcdot{}
  THEN  Auto)

---

Home Index