At: iter via intseg shift

  A:Type, f:(AAA), u:A, a,b,c,d:.
  b-a = d-c
  
  (e:({a..b}A), g:({c..d}A).
  ((i:{a..b}, j:{c..d}. j-i = c-a  e(i) = g(j))
  (
  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{c..d}. g(j)))

By:	SimilarTo 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))

1

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) i:{a..b}. e(i)) = (Iter(f;u) j:{c..d}. g(j))

4 steps

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