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