At: iter via intseg split mid

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

By:	Guarding (b:<type>. <prop>) Auto

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 :    b:, e:({a..b}A).   ac      cb      (Iter(f;u) i:{a..b}. e(i))   =   f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i))

16 steps

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