---

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


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]
BY
{ (RWO "member-list-to-set" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  list-to-set(eq;v)  \msim{}  v  supposing  no\_repeats(T;v)
6.  no\_repeats(T;v)  \mwedge{}  (\mneg{}(u  \mmember{}  v))
7.  (u  \mmember{}  list-to-set(eq;v))
\mvdash{}  list-to-set(eq;v)  \msim{}  [u  /  v]


By

---

Latex:
(RWO  "member-list-to-set"  (-1)  THEN  Auto)

---

Home Index