At: iter via intseg comp binop

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

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

1

1. A : Type 2. f : AAA 3. u : A 4. is_commutative_sep(A; f) 5. is_ident(A; f; u) 6. is_assoc_sep(A; f)   a,b:, e,g:({a..b}A).   f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i))   =   (Iter(f;u) i:{a..b}. f(e(i),g(i)))

14 steps

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