---

Step * of Lemma append_iseg

∀[T:Type]. ∀as,bs,cs:T List.  (as @ bs ≤ as @ cs ⇐⇒ bs ≤ cs)
BY
{ (Unfold `iseg` 0 THEN Auto THEN ParallelLast) }

1
1. T : Type
2. as : T List
3. bs : T List
4. cs : T List
5. l : T List
6. (as @ cs) = ((as @ bs) @ l) ∈ (T List)
⊢ cs = (bs @ l) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs,cs:T  List.    (as  @  bs  \mleq{}  as  @  cs  \mLeftarrow{}{}\mRightarrow{}  bs  \mleq{}  cs)


By

---

Latex:
(Unfold  `iseg`  0  THEN  Auto  THEN  ParallelLast)

---

Home Index