---

Step * 1 1 of Lemma list_accum_split

.....equality..... 
1. T : Type
2. i : ℤ
3. l : T List
⊢ firstn(0;l) ~ []
BY
{ ((((RecUnfold `firstn` 0 THEN Reduce 0) THEN ListInd (-1)) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  i  :  \mBbbZ{}
3.  l  :  T  List
\mvdash{}  firstn(0;l)  \msim{}  []


By

---

Latex:
((((RecUnfold  `firstn`  0  THEN  Reduce  0)  THEN  ListInd  (-1))  THEN  Reduce  0)  THEN  Auto)

---

Home Index