---

Step * 1 1 of Lemma tl_nth_tl


1. n : ℕ
2. L : Top List
3. nth_tl(1;nth_tl(n;L)) ~ nth_tl(1 + n;L)
4. X : Top
5. nth_tl(n;L) = X ∈ Top
⊢ tl(X) ~ nth_tl(1;X)
BY
{ (RecUnfold `nth_tl` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  Top  List
3.  nth\_tl(1;nth\_tl(n;L))  \msim{}  nth\_tl(1  +  n;L)
4.  X  :  Top
5.  nth\_tl(n;L)  =  X
\mvdash{}  tl(X)  \msim{}  nth\_tl(1;X)


By

---

Latex:
(RecUnfold  `nth\_tl`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index