---

Step * of Lemma remove-repeats-length-leq

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  (||remove-repeats(eq;L)|| ≤ ||L||)
BY
{ ((UnivCD THENA Auto) THEN ListInd (-1)) }

1
1. T : Type
2. eq : EqDecider(T)
⊢ ||remove-repeats(eq;[])|| ≤ ||[]||

2
1. T : Type
2. eq : EqDecider(T)
3. u : T@i
4. v : T List@i
5. ||remove-repeats(eq;v)|| ≤ ||v||@i
⊢ ||remove-repeats(eq;[u / v])|| ≤ ||[u / v]||

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  ListInd  (-1))

---

Home Index