---

Step * of Lemma list-to-set-property

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List.  (no_repeats(T;list-to-set(eq;L)) ∧ (∀a:T. ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `list-to-set` 0
   THEN D 0
   THEN Try ((BLemma `no_repeats_union` THEN Auto))
   THEN (((UnivCD THENA Auto) THEN RWO "member-union" 0) THENA Auto)) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. L : T List
4. a : T
⊢ (a ∈ []) ∨ (a ∈ L) ⇐⇒ (a ∈ L)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.
        (no\_repeats(T;list-to-set(eq;L))  \mwedge{}  (\mforall{}a:T.  ((a  \mmember{}  list-to-set(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `list-to-set`  0
  THEN  D  0
  THEN  Try  ((BLemma  `no\_repeats\_union`  THEN  Auto))
  THEN  (((UnivCD  THENA  Auto)  THEN  RWO  "member-union"  0)  THENA  Auto))

---

Home Index