---

Step * of Lemma concat_iseg

∀[T:Type]. ∀ll1,ll2:T List List.  (ll1 ≤ ll2 ⇒ concat(ll1) ≤ concat(ll2))
BY
{ ((Unfold `iseg` 0 THEN Auto THEN ExRepD THEN (HypSubst (-1) 0)) THENA Auto) }

1
1. [T] : Type
2. ll1 : T List List
3. ll2 : T List List
4. l : T List List
5. ll2 = (ll1 @ l) ∈ (T List List)
⊢ ∃l@0:T List. (concat(ll1 @ l) = (concat(ll1) @ l@0) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}ll1,ll2:T  List  List.    (ll1  \mleq{}  ll2  {}\mRightarrow{}  concat(ll1)  \mleq{}  concat(ll2))


By

---

Latex:
((Unfold  `iseg`  0  THEN  Auto  THEN  ExRepD  THEN  (HypSubst  (-1)  0))  THENA  Auto)

---

Home Index