Step
*
1
1
1
of Lemma
accum_list_cons_lemma
1. L : Top@i
2. u : Top@i
3. base : Top@i
4. f : Top@i
⊢ accumulate (with value a and list item y):
   f[a;y]
  over list:
    L
  with starting value:
   base[u]) ~ accumulate (with value a and list item y):
               f[a;y]
              over list:
                L
              with starting value:
               base[u])
BY
{ Try SqEqCD }
Latex:
Latex:
1.  L  :  Top@i
2.  u  :  Top@i
3.  base  :  Top@i
4.  f  :  Top@i
\mvdash{}  accumulate  (with  value  a  and  list  item  y):
      f[a;y]
    over  list:
        L
    with  starting  value:
      base[u])  \msim{}  accumulate  (with  value  a  and  list  item  y):
                              f[a;y]
                            over  list:
                                L
                            with  starting  value:
                              base[u])
By
Latex:
Try  SqEqCD
Home
Index