---

Step * of Lemma member-union

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀x:T.  ((x ∈ as ⋃ bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
BY
{ ((UnivCD THENA Auto) THEN Unfold `l-union` 0 THEN ListInd (-2) THEN Reduce 0) }

1
1. [T] : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. x : T@i
⊢ (x ∈ as) ⇐⇒ (x ∈ as) ∨ (x ∈ [])

2
1. [T] : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. x : T@i
5. u : T@i
6. v : T List@i
7. (x ∈ reduce(λa,L. insert(a;L);as;v)) ⇐⇒ (x ∈ as) ∨ (x ∈ v)@i
⊢ (x ∈ insert(u;reduce(λa,L. insert(a;L);as;v))) ⇐⇒ (x ∈ as) ∨ (x ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.  \mforall{}x:T.    ((x  \mmember{}  as  \mcup{}  bs)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as)  \mvee{}  (x  \mmember{}  bs))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `l-union`  0  THEN  ListInd  (-2)  THEN  Reduce  0)

---

Home Index