---

Step * 1 1 1 of Lemma combine-list-cons

.....equality..... 
1. A : Type
2. f : A ⟶ A ⟶ A
3. Assoc(A;λx,y. f[x;y])
4. a : A
5. u : A
6. v : A List
7. ∀u:A
     (accumulate (with value x and list item y):
       f[x;y]
      over list:
        v
      with starting value:
       f[a;u])
     = f[a;accumulate (with value x and list item y):
            f[x;y]
           over list:
             v
           with starting value:
            u)]
     ∈ A)
8. u@0 : A
⊢ f[f[a;u@0];u] = f[a;f[u@0;u]] ∈ A
BY
{ (Unfold `assoc` 3 THEN Reduce 3 THEN RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
3.  Assoc(A;\mlambda{}x,y.  f[x;y])
4.  a  :  A
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}u:A
          (accumulate  (with  value  x  and  list  item  y):
              f[x;y]
            over  list:
                v
            with  starting  value:
              f[a;u])
          =  f[a;accumulate  (with  value  x  and  list  item  y):
                        f[x;y]
                      over  list:
                          v
                      with  starting  value:
                        u)])
8.  u@0  :  A
\mvdash{}  f[f[a;u@0];u]  =  f[a;f[u@0;u]]


By

---

Latex:
(Unfold  `assoc`  3  THEN  Reduce  3  THEN  RWO  "3"  0  THEN  Auto)

---

Home Index