---

Step * of Lemma firstn_length

∀[L:Top List]. (firstn(||L||;L) ~ L)
BY
{ ((InductionOnList THEN RecUnfold `firstn` 0 THEN Reduce 0 THEN Try (Trivial) THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. u : Top
2. v : Top List
3. firstn(||v||;v) ~ v
4. 0 < ||v|| + 1
⊢ [u / firstn((||v|| + 1) - 1;v)] ~ [u / v]

2
.....falsecase..... 
1. u : Top
2. v : Top List
3. firstn(||v||;v) ~ v
4. (||v|| + 1) ≤ 0
⊢ [] ~ [u / v]

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  (firstn(||L||;L)  \msim{}  L)


By

---

Latex:
((InductionOnList  THEN  RecUnfold  `firstn`  0  THEN  Reduce  0  THEN  Try  (Trivial)  THEN  SplitOnConclITE)
  THENA  Auto
  )

---

Home Index