---

Step * 1 1 1 of Lemma set-equal-cons2


1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. bs : T List
6. ∀t:T. ((t ∈ [u / v]) ⇐⇒ (t ∈ bs))
7. (u ∈ bs)
8. t : T
9. (t ∈ [u / v]) ⇐⇒ (t ∈ bs)
⊢ (t ∈ filter(λx.(¬b(eq x u));v)) ⇐⇒ (t ∈ filter(λx.(¬b(eq x u));bs))
BY
{ ((RWO "cons_member" (-1) THENA Auto) THEN (RWO "member_filter" 0 THENM Reduce 0) THEN Auto) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. bs : T List
6. ∀t:T. ((t ∈ [u / v]) ⇐⇒ (t ∈ bs))
7. (u ∈ bs)
8. t : T
9. ((t = u ∈ T) ∨ (t ∈ v)) ⇒ (t ∈ bs)
10. ((t = u ∈ T) ∨ (t ∈ v)) ⇐ (t ∈ bs)
11. (t ∈ bs)
12. ↑¬b(eq t u)
⊢ (t ∈ v)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  bs  :  T  List
6.  \mforall{}t:T.  ((t  \mmember{}  [u  /  v])  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  bs))
7.  (u  \mmember{}  bs)
8.  t  :  T
9.  (t  \mmember{}  [u  /  v])  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  bs)
\mvdash{}  (t  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));bs))


By

---

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

---

Home Index