---

Step * of Lemma list-list-concat-type

∀[T:Type]. ∀[L:T List List].  (L ∈ {x:T| (x ∈ concat(L))}  List List)
BY
{ InductionOnList }

1
1. T : Type
⊢ [] ∈ {x:T| (x ∈ concat([]))}  List List

2
1. T : Type
2. u : T List
3. v : T List List
4. v ∈ {x:T| (x ∈ concat(v))}  List List
⊢ [u / v] ∈ {x:T| (x ∈ concat([u / v]))}  List List

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List  List].    (L  \mmember{}  \{x:T|  (x  \mmember{}  concat(L))\}    List  List)


By

---

Latex:
InductionOnList

---

Home Index