Step
*
1
2
1
of Lemma
member-concat
1. [T] : Type
2. u : T List
3. v : T List List
4. ∀x:T. ((x ∈ concat(v))
⇐⇒ ∃l:T List. ((l ∈ v) ∧ (x ∈ l)))
5. x : T
6. (x ∈ concat(v))
7. ∃l:T List. ((l ∈ v) ∧ (x ∈ l))
⊢ ∃l:T List. (((l = u ∈ (T List)) ∨ (l ∈ v)) ∧ (x ∈ l))
BY
{ (ParallelLast THEN Auto) }
Latex:
Latex:
1. [T] : Type
2. u : T List
3. v : T List List
4. \mforall{}x:T. ((x \mmember{} concat(v)) \mLeftarrow{}{}\mRightarrow{} \mexists{}l:T List. ((l \mmember{} v) \mwedge{} (x \mmember{} l)))
5. x : T
6. (x \mmember{} concat(v))
7. \mexists{}l:T List. ((l \mmember{} v) \mwedge{} (x \mmember{} l))
\mvdash{} \mexists{}l:T List. (((l = u) \mvee{} (l \mmember{} v)) \mwedge{} (x \mmember{} l))
By
Latex:
(ParallelLast THEN Auto)
Home
Index