Step * 1 1 of Lemma list_accum_split

.....equality..... 
1. Type
2. : ℤ
3. List
⊢ firstn(0;l) []
BY
((((RecUnfold `firstn` 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