---

Step * of Lemma length-remove-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
  ||remove-repeats(eq;L1)|| = ||remove-repeats(eq;L2)|| ∈ ℤ supposing ∀x:T. ((x ∈ L1) ⇐⇒ (x ∈ L2))
BY
{ Auto
THEN BLemma `set-equal-no_repeats-length`
THEN Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. L1 : T List
4. L2 : T List
5. ∀x:T. ((x ∈ L1) ⇐⇒ (x ∈ L2))
⊢ set-equal(T;remove-repeats(eq;L1);remove-repeats(eq;L2))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L1,L2:T  List].
    ||remove-repeats(eq;L1)||  =  ||remove-repeats(eq;L2)||  supposing  \mforall{}x:T.  ((x  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2))


By

---

Latex:
Auto
THEN  BLemma  `set-equal-no\_repeats-length`
THEN  Auto

---

Home Index