---

Step * of Lemma nth_tl_map

∀[f:Top]. ∀[n:ℕ]. ∀[l:Top List].  (nth_tl(n;map(f;l)) ~ map(f;nth_tl(n;l)))
BY
{ InductionOnNat }

1
.....basecase..... 
1. f : Top
2. n : ℤ
⊢ ∀[l:Top List]. (nth_tl(0;map(f;l)) ~ map(f;nth_tl(0;l)))

2
.....upcase..... 
1. f : Top
2. n : ℤ
3. 0 < n
4. ∀[l:Top List]. (nth_tl(n - 1;map(f;l)) ~ map(f;nth_tl(n - 1;l)))
⊢ ∀[l:Top List]. (nth_tl(n;map(f;l)) ~ map(f;nth_tl(n;l)))

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[l:Top  List].    (nth\_tl(n;map(f;l))  \msim{}  map(f;nth\_tl(n;l)))


By

---

Latex:
InductionOnNat

---

Home Index