---

Step * of Lemma iseg_append_length

∀[T:Type]. ∀l1,l2,l3:T List.  (l1 ≤ l2 @ l3 ⇒ l1 ≤ l2 supposing ||l1|| ≤ ||l2||)
BY
{ (((Auto
     THEN (RWO "iseg_append_iff" (-2))
     THEN Auto
     THEN (D (-2))
     THEN Auto
     THEN ExRepD
     THEN (ApFunToHypEquands `Z' ⌜||Z||⌝ ⌜ℤ⌝ (-3))⋅)
    THENA Auto
    )
   THEN (RWO "length_append" (-1))
   THEN Auto') }

---

Latex:

---

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


By

---

Latex:
(((Auto
      THEN  (RWO  "iseg\_append\_iff"  (-2))
      THEN  Auto
      THEN  (D  (-2))
      THEN  Auto
      THEN  ExRepD
      THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}||Z||\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-3))\mcdot{})
    THENA  Auto
    )
  THEN  (RWO  "length\_append"  (-1))
  THEN  Auto')

---

Home Index