---

Step * of Lemma nth_tl_is_fseg

∀[T:Type]. ∀L1,L2:T List.  (fseg(T;L1;L2) ⇐⇒ ∃n:ℕ||L2|| + 1. (L1 = nth_tl(n;L2) ∈ (T List)))
BY
{ ((Unfold `fseg` 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)
⊢ ∃n:ℕ||L2|| + 1. (L1 = nth_tl(n;L2) ∈ (T List))

2
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. n : ℕ||L2|| + 1
5. L1 = nth_tl(n;L2) ∈ (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{}  \mexists{}n:\mBbbN{}||L2||  +  1.  (L1  =  nth\_tl(n;L2)))


By

---

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

---

Home Index