---

Step * 1 2 1 of Lemma list_accum_split

.....equality..... 
1. T : Type
2. i : ℤ
3. l : T List
4. f : Top ⟶ T ⟶ Top
5. y : Top
⊢ accumulate (with value x and list item a):
   f[x;a]
  over list:
    []
  with starting value:
   y) ~ y
BY
{ ((RecUnfold `list_accum` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  i  :  \mBbbZ{}
3.  l  :  T  List
4.  f  :  Top  {}\mrightarrow{}  T  {}\mrightarrow{}  Top
5.  y  :  Top
\mvdash{}  accumulate  (with  value  x  and  list  item  a):
      f[x;a]
    over  list:
        []
    with  starting  value:
      y)  \msim{}  y


By

---

Latex:
((RecUnfold  `list\_accum`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index