---

Step * of Lemma nth_tl_factor

∀T:Type. ∀n:ℕ. ∀as:T List.  ((n ≤ ||as||) ⇒ (nth_tl(n;as) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)))
BY
{ ((CDToVarThen `n' NatInd THENA Auto) THEN ((RecCaseSplit `nth_tl`) THEN Auto)) }

1
1. T : Type
2. 0 ≤ 0
3. as : T List
4. 0 ≤ ||as||
⊢ as = (Π 0 ≤ i < ||as||. [as[i]]) ∈ (T List)

2
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||
⊢ nth_tl(n - 1;tl(as)) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}n:\mBbbN{}.  \mforall{}as:T  List.    ((n  \mleq{}  ||as||)  {}\mRightarrow{}  (nth\_tl(n;as)  =  (\mPi{}  n  \mleq{}  i  <  ||as||.  [as[i]])))


By

---

Latex:
((CDToVarThen  `n'  NatInd  THENA  Auto)  THEN  ((RecCaseSplit  `nth\_tl`)  THEN  Auto))

---

Home Index