At: iter via intseg split pluck

  A:Type, f:(AAA), u:A.
  is_ident(A; f; u)
  
  is_assoc_sep(A; f)
  
  (a,c,b:, e:({a..b}A).
  (ac
  (
  (c<b
  (
  ((Iter(f;u) i:{a..b}. e(i))
  (=
  (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. 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. c :  8. b :  9. e : {a..b}A 10. ac 11. c<b 12. (Iter(f;u) i:{a..b}. e(i)) 12. = 12. f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i))   (Iter(f;u) i:{a..b}. e(i))   =   f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i)))

5 steps

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