---

Step * of Lemma length_nth_tl

No Annotations
∀[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}].  (||nth_tl(n;as)|| = (||as|| - n) ∈ ℤ)
BY
{ (InductionOnList THEN ((Reduce 0 THENM D 0) THENM RecCaseSplit `nth_tl`) THEN Auto') }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[as:A  List].  \mforall{}[n:\{0...||as||\}].    (||nth\_tl(n;as)||  =  (||as||  -  n))


By

---

Latex:
(InductionOnList  THEN  ((Reduce  0  THENM  D  0)  THENM  RecCaseSplit  `nth\_tl`)  THEN  Auto')

---

Home Index