---

Step * 2 of Lemma no-repeats-iff-count


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
⊢ no_repeats(T;L)
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;L)||;||filter(eq  x;L)||  =  1)
\mvdash{}  no\_repeats(T;L)


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index