---

Step * of Lemma fseg-iseg-reverse

∀[T:Type]. ∀[L1,L2:T List].  (fseg(T;L1;L2) ⇐⇒ rev(L1) ≤ rev(L2))
BY
{ (RepUR ``fseg iseg`` 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. [L1] : T List
3. [L2] : T List
4. L : T List
5. L2 = (L @ L1) ∈ (T List)
⊢ ∃l:T List. (rev(L2) = (rev(L1) @ l) ∈ (T List))

2
1. [T] : Type
2. [L1] : T List
3. [L2] : T List
4. l : T List
5. rev(L2) = (rev(L1) @ l) ∈ (T List)
⊢ ∃L:T List. (L2 = (L @ L1) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].    (fseg(T;L1;L2)  \mLeftarrow{}{}\mRightarrow{}  rev(L1)  \mleq{}  rev(L2))


By

---

Latex:
(RepUR  ``fseg  iseg``  0  THEN  Auto  THEN  ExRepD)

---

Home Index