---

Step * 1 of Lemma nth_tl-append


∀[bs:Top]. ∀n:ℕ. (nth_tl(n;bs) ~ if n <z 0 then nth_tl(n;[]) @ bs else nth_tl(n - 0;bs) fi )
BY
{ (Auto THEN AutoSplit) }

---

Latex:

---

Latex:

\mforall{}[bs:Top].  \mforall{}n:\mBbbN{}.  (nth\_tl(n;bs)  \msim{}  if  n  <z  0  then  nth\_tl(n;[])  @  bs  else  nth\_tl(n  -  0;bs)  fi  )


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index