sig
  type ('a, 'b) sum = Left of 'a | Right of 'b
  val sum_of_coqsum :
    (Constr.constr -> 'a) ->
    (Constr.constr -> 'b) -> Constr.constr -> ('a, 'b) Coqsum.sum
  val sum_to_coqsum :
    Constr.constr ->
    ('a -> Constr.constr) ->
    Constr.constr ->
    ('b -> Constr.constr) -> ('a, 'b) Coqsum.sum -> Constr.constr
end