---

Step * 2 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. 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)
BY
{ ((D (-1) THEN D 0 THEN ProveProp) THEN Auto) }

---

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.  cs  :  T  List
8.  ds  :  T  List
9.  bs  =  (cs  @  [u  /  ds])
10.  \mforall{}t:T.  ((t  \mmember{}  v)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  cs  @  ds))
11.  t  :  T
12.  (t  \mmember{}  v)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  cs)  \mvee{}  (t  \mmember{}  ds)
\mvdash{}  (t  =  u)  \mvee{}  (t  \mmember{}  v)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  cs)  \mvee{}  (t  =  u)  \mvee{}  (t  \mmember{}  ds)


By

---

Latex:
((D  (-1)  THEN  D  0  THEN  ProveProp)  THEN  Auto)

---

Home Index