At: iter via intseg notnull

  A:Type, f:(AAA), u:A, a,b:, e:({a..b}A).
  a<b
  
  (c:. 
  (b = c+1
  (
  ((Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c)))

1

1. A : Type 2. f : AAA 3. u : A 4. a :  5. b :  6. e : {a..b}A 7. a<b 8. c :  9. b = c+1   (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c))

2 steps

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