---

Step * of Lemma iseg_append0

∀[T:Type]. ∀l1,l2:T List.  l1 ≤ l1 @ l2
BY
{ (((Unfold `iseg` 0 THEN Auto) THEN InstConcl [l2]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2:T  List.    l1  \mleq{}  l1  @  l2


By

---

Latex:
(((Unfold  `iseg`  0  THEN  Auto)  THEN  InstConcl  [l2])  THEN  Auto)

---

Home Index