---

Step * of Lemma fseg_length

∀[T:Type]. ∀[l1,l2:T List].  ||l1|| ≤ ||l2|| supposing fseg(T;l1;l2)
BY
{ (((((Unfold `fseg` 0 THEN Auto) THEN ExRepD) THEN HypSubst (-1) 0) THEN Auto) THEN RWO "length_append" 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].    ||l1||  \mleq{}  ||l2||  supposing  fseg(T;l1;l2)


By

---

Latex:
(((((Unfold  `fseg`  0  THEN  Auto)  THEN  ExRepD)  THEN  HypSubst  (-1)  0)  THEN  Auto)
  THEN  RWO  "length\_append"  0
  THEN  Auto')

---

Home Index