---

Step * 1 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 ∈ T) ∨ (t ∈ v)) ⇒ (t ∈ bs)
10. ((t = u ∈ T) ∨ (t ∈ v)) ⇐ (t ∈ bs)
11. (t ∈ bs)
12. ↑¬b(eq t u)
⊢ (t ∈ v)
BY
{ (RW assert_pushdownC (-1) THEN Auto THEN (D -3 THENA Auto) THEN D -1 THEN Auto) }

---

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  =  u)  \mvee{}  (t  \mmember{}  v))  {}\mRightarrow{}  (t  \mmember{}  bs)
10.  ((t  =  u)  \mvee{}  (t  \mmember{}  v))  \mLeftarrow{}{}  (t  \mmember{}  bs)
11.  (t  \mmember{}  bs)
12.  \muparrow{}\mneg{}\msubb{}(eq  t  u)
\mvdash{}  (t  \mmember{}  v)


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto  THEN  (D  -3  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index