---

Step * 1 of Lemma length-lastn


1. A : Type
2. L : A List
3. n : ℕ
4. n ≤ ||L||
⊢ ||nth_tl(||L|| - n;L)|| = n ∈ ℤ
BY
{ (RWO "length_nth_tl" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  n  :  \mBbbN{}
4.  n  \mleq{}  ||L||
\mvdash{}  ||nth\_tl(||L||  -  n;L)||  =  n


By

---

Latex:
(RWO  "length\_nth\_tl"  0  THEN  Auto')

---

Home Index