let vars_of (a, _) =
  match a with 
    | TT -> Term.Var.Set.empty
    | FF -> Term.Var.Set.empty
    | Equal(a, b) -> Term.Var.Set.union (Term.vars_of a) (Term.vars_of b)
    | Diseq(a, b) -> Term.Var.Set.union (Term.vars_of a) (Term.vars_of b)
    | Nonneg(a) -> Term.vars_of a
    | Pos(a) -> Term.vars_of a