At: iter via intseg amputate units

  A:Type, f:(AAA), u:A.
  is_ident(A; f; u)
  
  is_assoc_sep(A; f)
  
  (a,b:, c:{a...b}, d:{c..b}, e:({a..b}A).
  ((i:{a..b}. i<c  di  e(i) = u)
  (
  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))

1

1. A : Type 2. f : AAA 3. u : A 4. is_ident(A; f; u) 5. is_assoc_sep(A; f) 6. a :  7. b :  8. c : {a...b} 9. d : {c..b} 10. e : {a..b}A 11. i:{a..b}. i<c  di  e(i) = u   (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i))

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html