---

Step * of Lemma member-l-union-list

∀[T:Type]. ∀eq:EqDecider(T). ∀ll:T List List. ∀x:T.  ((x ∈ l-union-list(eq;ll)) ⇐⇒ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l)))
BY
{ (InductionOnList THEN Unfold `l-union-list` 0 THEN Reduce 0 THEN Try (Fold `l-union-list` 0⋅)) }

1
1. [T] : Type
2. eq : EqDecider(T)
⊢ ∀x:T. ((x ∈ []) ⇐⇒ ∃l:T List. ((l ∈ []) ∧ (x ∈ l)))

2
1. [T] : Type
2. eq : EqDecider(T)
3. u : T List
4. v : T List List
5. ∀x:T. ((x ∈ l-union-list(eq;v)) ⇐⇒ ∃l:T List. ((l ∈ v) ∧ (x ∈ l)))
⊢ ∀x:T. ((x ∈ l-union-list(eq;v) ⋃ u) ⇐⇒ ∃l:T List. ((l ∈ [u / v]) ∧ (x ∈ l)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}ll:T  List  List.  \mforall{}x:T.
        ((x  \mmember{}  l-union-list(eq;ll))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}l:T  List.  ((l  \mmember{}  ll)  \mwedge{}  (x  \mmember{}  l)))


By

---

Latex:
(InductionOnList  THEN  Unfold  `l-union-list`  0  THEN  Reduce  0  THEN  Try  (Fold  `l-union-list`  0\mcdot{}))

---

Home Index