1. i : 
2. x : 
3. y : 
4. xy
  ixiy = i(x+y)

By:	Rewrite by Thm*  f:(AAA), u:A, a,b:, e:({a..b}A), k:. Thm*  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k)) Using:[A:=  | f:= x,y. xy | u:= 1 | a:= 0 | e(z):= i | b:= y | k:= x] THEN ArithSimp Concl

1

ix( j:{x..x+y}. i) = i(x+y)

1 step

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