---

Step * of Lemma no-repeats-iff-count

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].
  uiff(no_repeats(T;L);∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
5. x : T
6. 1 ≤ ||filter(eq x;L)||
⊢ ||filter(eq x;L)|| = 1 ∈ ℤ

2
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)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index