let negate = function
  | True -> mk_false
  | False -> mk_true
  | Equal(a, b) -> mk_diseq (a, b)
  | Diseq(a, b) -> mk_equal (a, b)
  | In(a, s) when Sign.complementable s -> mk_in (a, Sign.complement s)
  | a ->
      let str = Pretty.to_string pp a in
        raise (Invalid_argument ("Atom " ^ str ^ " not negatable."))