---

Step * of Lemma length-remove-repeats-le

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  (||remove-repeats(eq;L)|| ≤ ||L||)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RWO "length-filter" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].    (||remove-repeats(eq;L)||  \mleq{}  ||L||)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  RWO  "length-filter"  0  THEN  Auto)

---

Home Index