---

Step * 1 1 1 1 1 1 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. set-equal(T;[u / v];bs)
8. (u ∈ bs)
9. l1 : T List
10. l2 : T List
11. bs = (l1 @ [u / l2]) ∈ (T List)
12. bs = (l1 @ [u / l2]) ∈ (T List)
13. ∀t:T. ((t ∈ [u / v]) ⇐⇒ (t ∈ l1 @ [u / l2]))
14. t : T
15. (t ∈ [u / v]) ⇐⇒ (t ∈ l1 @ [u / l2])
⊢ (t ∈ v) ⇐⇒ (t ∈ l1 @ l2)
BY
{ ((RWO "member_append" 0 THENM RWO "member_append" (-1) THENM RWO "cons_member" (-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. set-equal(T;[u / v];bs)
8. (u ∈ bs)
9. l1 : T List
10. l2 : T List
11. bs = (l1 @ [u / l2]) ∈ (T List)
12. bs = (l1 @ [u / l2]) ∈ (T List)
13. ∀t:T. ((t ∈ [u / v]) ⇐⇒ (t ∈ l1 @ [u / l2]))
14. t : T
15. (t = u ∈ T) ∨ (t ∈ v) ⇐⇒ (t ∈ l1) ∨ (t = u ∈ T) ∨ (t ∈ l2)
⊢ (t ∈ v) ⇐⇒ (t ∈ l1) ∨ (t ∈ l2)

---

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.  set-equal(T;[u  /  v];bs)
8.  (u  \mmember{}  bs)
9.  l1  :  T  List
10.  l2  :  T  List
11.  bs  =  (l1  @  [u  /  l2])
12.  bs  =  (l1  @  [u  /  l2])
13.  \mforall{}t:T.  ((t  \mmember{}  [u  /  v])  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  l1  @  [u  /  l2]))
14.  t  :  T
15.  (t  \mmember{}  [u  /  v])  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  l1  @  [u  /  l2])
\mvdash{}  (t  \mmember{}  v)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  l1  @  l2)


By

---

Latex:
((RWO  "member\_append"  0  THENM  RWO  "member\_append"  (-1)  THENM  RWO  "cons\_member"  (-1))  THENA  Auto)

---

Home Index