---

Step * of Lemma append_firstn_lastn

∀[T:Type]. ∀[L:T List]. ∀[n:{0...||L||}].  ((firstn(n;L) @ nth_tl(n;L)) = L ∈ (T List))
BY
{ (InductionOnList
   THEN Auto
   THEN Reduce (-1)
   THEN RecUnfold `firstn` 0
   THEN RecUnfold `nth_tl` 0
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 (AutoSplit)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[n:\{0...||L||\}].    ((firstn(n;L)  @  nth\_tl(n;L))  =  L)


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  RecUnfold  `firstn`  0
  THEN  RecUnfold  `nth\_tl`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  (AutoSplit)
  THEN  EqCD
  THEN  Auto)

---

Home Index