1. A : Type
2. f : AAA
3. u : A
4. a : 
5. b : 
6. e:({a..b}A), k:.
6. (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))
7. c : 
8. d : 
9. b-a = d-c
10. e : {a..b}A
11. g : {c..d}A
12. i:{a..b}, j:{c..d}. j-i = c-a  e(i) = g(j)
  (Iter(f;u) j:{a+c-a..b+c-a}. e(j-(c-a))) = (Iter(f;u) j:{c..d}. g(j))

1

13. j : {(a+c-a)..(b+c-a)}   e(j-(c-a)) = g(j)

2 steps

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