---

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


1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ no_repeats(T;L) supposing ||remove-repeats(eq;L)|| = ||L|| ∈ ℤ
BY
{ (Auto THEN ListInd (-2)) }

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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
\mvdash{}  no\_repeats(T;L)  supposing  ||remove-repeats(eq;L)||  =  ||L||


By

---

Latex:
(Auto  THEN  ListInd  (-2))

---

Home Index