---

Step * of Lemma select-nth_tl

∀[n,x:ℕ]. ∀[L:Top List].  (nth_tl(n;L)[x] ~ L[n + x])
BY
{ (InductionOnNat
   THEN RecUnfold `nth_tl` 0
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN Try ((EqCD THEN Complete (Auto)))
   THEN AutoSplit
   THEN (RWO "-3" 0 THENA Auto)) }

1
1. n : ℤ
2. ¬(n ≤ 0)
3. 0 < n
4. ∀[x:ℕ]. ∀[L:Top List].  (nth_tl(n - 1;L)[x] ~ L[(n - 1) + x])
5. x : ℕ
6. L : Top List
⊢ tl(L)[(n - 1) + x] ~ L[n + x]

---

Latex:

---

Latex:
\mforall{}[n,x:\mBbbN{}].  \mforall{}[L:Top  List].    (nth\_tl(n;L)[x]  \msim{}  L[n  +  x])


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `nth\_tl`  0
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((EqCD  THEN  Complete  (Auto)))
  THEN  AutoSplit
  THEN  (RWO  "-3"  0  THENA  Auto))

---

Home Index