---

Step * of Lemma no-repeats-list-to-set

∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List.  list-to-set(eq;L) ~ L supposing no_repeats(T;L)
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (RWO "no_repeats_cons" (-1) THENA Auto)
   THEN (RWO "list-to-set-cons" 0 THENA Auto)
   THEN AutoSplit) }

1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. list-to-set(eq;v) ~ v supposing no_repeats(T;v)
6. no_repeats(T;v) ∧ (¬(u ∈ v))
7. (u ∈ list-to-set(eq;v))
⊢ list-to-set(eq;v) ~ [u / v]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.    list-to-set(eq;L)  \msim{}  L  supposing  no\_repeats(T;L)


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "no\_repeats\_cons"  (-1)  THENA  Auto)
  THEN  (RWO  "list-to-set-cons"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index