---

Step * of Lemma firstn-firstn

No Annotations
∀[L:Top List]. ∀[n:ℕ]. ∀[m:ℕn].  (firstn(m;firstn(n;L)) ~ firstn(m;L))
BY
{ (InductionOnList
   THEN RecUnfold `firstn` 0
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 (AutoSplit)
   THEN EqCD
   THEN Try (BackThruSomeHyp)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n].    (firstn(m;firstn(n;L))  \msim{}  firstn(m;L))


By

---

Latex:
(InductionOnList
  THEN  RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  (AutoSplit)
  THEN  EqCD
  THEN  Try  (BackThruSomeHyp)
  THEN  Auto)

---

Home Index