---

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

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

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

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0)

---

Home Index