---

Step * of Lemma remove-repeats-length-one

∀T:Type. ∀eq:EqDecider(T). ∀L:T List.
  (||remove-repeats(eq;L)|| = 1 ∈ ℤ ⇐⇒ ∃x:T. ((x ∈ L) ∧ (∀y:T. y = x ∈ T supposing (y ∈ L))))
BY
{ (Auto THEN (Assert set-equal(T;remove-repeats(eq;L);L) BY Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ||remove-repeats(eq;L)|| = 1 ∈ ℤ
5. set-equal(T;remove-repeats(eq;L);L)
⊢ ∃x:T. ((x ∈ L) ∧ (∀y:T. y = x ∈ T supposing (y ∈ L)))

2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∃x:T. ((x ∈ L) ∧ (∀y:T. y = x ∈ T supposing (y ∈ L)))
5. set-equal(T;remove-repeats(eq;L);L)
⊢ ||remove-repeats(eq;L)|| = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.
    (||remove-repeats(eq;L)||  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:T.  ((x  \mmember{}  L)  \mwedge{}  (\mforall{}y:T.  y  =  x  supposing  (y  \mmember{}  L))))


By

---

Latex:
(Auto  THEN  (Assert  set-equal(T;remove-repeats(eq;L);L)  BY  Auto))

---

Home Index