---

Step * of Lemma firstn_is_iseg

∀[T:Type]. ∀L1,L2:T List.  (L1 ≤ L2 ⇐⇒ ∃n:ℕ||L2|| + 1. (L1 = firstn(n;L2) ∈ (T List)))
BY
{ ((Unfold `iseg` 0 THEN Auto) THEN ExRepD) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. l : T List
5. L2 = (L1 @ l) ∈ (T List)
⊢ ∃n:ℕ||L2|| + 1. (L1 = firstn(n;L2) ∈ (T List))

2
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. n : ℕ||L2|| + 1
5. L1 = firstn(n;L2) ∈ (T List)
⊢ ∃l:T List. (L2 = (L1 @ l) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    (L1  \mleq{}  L2  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}||L2||  +  1.  (L1  =  firstn(n;L2)))


By

---

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

---

Home Index