---

Step * of Lemma length_firstn

∀[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}].  (||firstn(n;as)|| ~ n)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RecCaseSplit `firstn` THEN Auto' THEN RWO "-3" 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as:A  List].  \mforall{}[n:\{0...||as||\}].    (||firstn(n;as)||  \msim{}  n)


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  RecCaseSplit  `firstn`
  THEN  Auto'
  THEN  RWO  "-3"  0
  THEN  Auto')

---

Home Index