---

Step * of Lemma nth_tl_is_nil

∀[n:ℕ]. ∀[L:Top List].  nth_tl(n;L) ~ [] supposing ||L|| ≤ n
BY
{ (InductionOnNat THEN Reduce 0) }

1
1. n : ℤ
⊢ ∀[L:Top List]. L ~ [] supposing ||L|| ≤ 0

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[L:Top List]. nth_tl(n - 1;L) ~ [] supposing ||L|| ≤ (n - 1)
⊢ ∀[L:Top List]. nth_tl(n;L) ~ [] supposing ||L|| ≤ n

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:Top  List].    nth\_tl(n;L)  \msim{}  []  supposing  ||L||  \mleq{}  n


By

---

Latex:
(InductionOnNat  THEN  Reduce  0)

---

Home Index