---

Step * 2 of Lemma set-equal-cons


1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ set-equal(T;v;cs @ ds))
⊢ set-equal(T;[u / v];bs)
BY
{ (((ExRepD THEN (HypSubst' -2 0 THENA Auto)) THEN RepeatFor 2 (ParallelLast))
   THEN ((RWO "cons_member" 0 THENM RWO "member_append" 0 THENM RWO "cons_member" 0) THENA Auto)
   THEN (RWO "member_append" (-1) THENA Auto)) }

1
1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. cs : T List
8. ds : T List
9. bs = (cs @ [u / ds]) ∈ (T List)
10. ∀t:T. ((t ∈ v) ⇐⇒ (t ∈ cs @ ds))
11. t : T
12. (t ∈ v) ⇐⇒ (t ∈ cs) ∨ (t ∈ ds)
⊢ (t = u ∈ T) ∨ (t ∈ v) ⇐⇒ (t ∈ cs) ∨ (t = u ∈ T) ∨ (t ∈ ds)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  bs  :  T  List
5.  no\_repeats(T;[u  /  v])
6.  no\_repeats(T;bs)
7.  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  set-equal(T;v;cs  @  ds))
\mvdash{}  set-equal(T;[u  /  v];bs)


By

---

Latex:
(((ExRepD  THEN  (HypSubst'  -2  0  THENA  Auto))  THEN  RepeatFor  2  (ParallelLast))
  THEN  ((RWO  "cons\_member"  0  THENM  RWO  "member\_append"  0  THENM  RWO  "cons\_member"  0)  THENA  Auto)
  THEN  (RWO  "member\_append"  (-1)  THENA  Auto))

---

Home Index