---

Step * 2 1 of Lemma nth_tl_factor


1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (nth_tl(n - 1;as) = (Π n - 1 ≤ i < ||as||. [as[i]]) ∈ (T List)))
5. 0 < n
6. as : T List
7. n ≤ ||as||
8. ||as|| ≥ 1 
⊢ (Π n - 1 ≤ i < ||tl(as)||. [tl(as)[i]]) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)
BY
{ (RWO "select_tl length_tl" 0 THENA Auto) }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (nth_tl(n - 1;as) = (Π n - 1 ≤ i < ||as||. [as[i]]) ∈ (T List)))
5. 0 < n
6. as : T List
7. n ≤ ||as||
8. ||as|| ≥ 1 
⊢ (Π n - 1 ≤ i < ||as|| - 1. [as[i + 1]]) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}as:T  List.  (((n  -  1)  \mleq{}  ||as||)  {}\mRightarrow{}  (nth\_tl(n  -  1;as)  =  (\mPi{}  n  -  1  \mleq{}  i  <  ||as||.  [as[i]])))
5.  0  <  n
6.  as  :  T  List
7.  n  \mleq{}  ||as||
8.  ||as||  \mgeq{}  1 
\mvdash{}  (\mPi{}  n  -  1  \mleq{}  i  <  ||tl(as)||.  [tl(as)[i]])  =  (\mPi{}  n  \mleq{}  i  <  ||as||.  [as[i]])


By

---

Latex:
(RWO  "select\_tl  length\_tl"  0  THENA  Auto)

---

Home Index