---

Step * of Lemma remove-repeats-length-no-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  ||remove-repeats(eq;L)|| = ||L|| ∈ ℤ supposing no_repeats(T;L)
BY
{ ((UnivCD THENA Auto) THEN ListInd (-2)) }

1
1. T : Type
2. eq : EqDecider(T)
⊢ no_repeats(T;[]) ⇒ (||remove-repeats(eq;[])|| = ||[]|| ∈ ℤ)

2
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;v) ⇒ (||remove-repeats(eq;v)|| = ||v|| ∈ ℤ)
⊢ no_repeats(T;[u / v]) ⇒ (||remove-repeats(eq;[u / v])|| = ||[u / v]|| ∈ ℤ)

---

Latex:

---

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


By

---

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

---

Home Index