theory Sum

  type sum 'a 'b =
    | Left 'a
    | Right 'b

end