At: sum via intseg split pluck

  a,c,b:, e:({a..b}).
  ac
  
  c<b  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))

By:

Inst:  Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,c,b:, e:({a..b}A). Thm*  (ac Thm*  ( Thm*  (c<b Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) Thm*  (= Thm*  (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i)))) Using:[ | x,y. x+y | 0] THEN OnAllClauses Reduce

1	is_ident(; (x,y. x+y); 0)	2 steps
2	is_assoc_sep(; (x,y. x+y))	2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html