---

Step * 1 of Lemma length-remove-repeats


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))
BY
{ Unfold `set-equal` 0
THEN (RWO "member-remove-repeats" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L1  :  T  List
4.  L2  :  T  List
5.  \mforall{}x:T.  ((x  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2))
\mvdash{}  set-equal(T;remove-repeats(eq;L1);remove-repeats(eq;L2))


By

---

Latex:
Unfold  `set-equal`  0
THEN  (RWO  "member-remove-repeats"  0  THEN  Auto)

---

Home Index