let rec variables = function
| True | False -> Variable.Set.empty
| Comp (t1, _, t2) ->
Variable.Set.union (Term.variables t1) (Term.variables t2)
| Ite (sa, a1, a2) ->
let acc = Variable.Set.union (variables a1) (variables a2) in
Variable.Set.union acc (SAtom.variables sa)