[PostScript]
ReduceContainer (unit, \circ): trait
  % Insert the operator in enumeration order.
  assumes Container
  introduces 
    unit: -> E
    __ \circ __: E, E -> E
    reduce: C -> E
  asserts forall c: C
    reduce(c) ==
      if c = empty then unit
      else head(c) \circ reduce(tail(c))
  implies converts reduce
[Table of Contents] [Index]