---

Step * of Lemma nth_tl_nil

∀[n:ℤ]. (nth_tl(n;[]) ~ [])
BY
{ ((D 0 THENA Auto)
   THEN IntInd0 (-1)
   THEN Try ((Reduce 0 THEN Trivial))
   THEN RecUnfold `nth_tl` 0
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (nth\_tl(n;[])  \msim{}  [])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  IntInd0  (-1)
  THEN  Try  ((Reduce  0  THEN  Trivial))
  THEN  RecUnfold  `nth\_tl`  0
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index