---

Step * of Lemma concat-decomp

∀[T:Type]
  ∀ll:T List List. ∀x:T.
    ((x ∈ concat(ll))
    ⇐⇒ ∃ll1,ll2:T List List
         ∃l1,l2:T List
          ((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List))
          ∧ (ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List))))
BY
{ TACTIC:(Intros THEN RWO "member-concat" 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. ll : T List List
3. x : T
4. l : T List
5. (l ∈ ll)
6. (x ∈ l)
⊢ ∃ll1,ll2:T List List
   ∃l1,l2:T List
    ((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List))
    ∧ (ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List)))

2
1. [T] : Type
2. ll : T List List
3. x : T
4. ll1 : T List List
5. ll2 : T List List
6. l1 : T List
7. l2 : T List
8. concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List)
9. ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List)
⊢ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}ll:T  List  List.  \mforall{}x:T.
        ((x  \mmember{}  concat(ll))
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}ll1,ll2:T  List  List
                  \mexists{}l1,l2:T  List
                    ((concat(ll)  =  (concat(ll1)  @  (l1  @  [x]  @  l2)  @  concat(ll2)))
                    \mwedge{}  (ll  =  (ll1  @  [l1  @  [x]  @  l2]  @  ll2))))


By

---

Latex:
TACTIC:(Intros  THEN  RWO  "member-concat"  0  THEN  Auto  THEN  ExRepD)

---

Home Index