let mk_in (a, c) =
  match c with
    | Sign.F -> mk_false
    | Sign.Zero -> mk_equal (a, Arith.mk_zero)
    | _ ->
        (match Arith.d_num a with
           | Some(q) -> 
               if Sign.mem q c then mk_true else mk_false
           | None ->
               In(a, c))