let rec solve (a, b) =
  solve1 (mk_iff a b) []

and solve1 a sl =
  try
    (match d_interp a with
      | Sym.Empty, [] -> raise Exc.Inconsistent
      | Sym.Full, [] -> sl
      | Sym.Ite, [x; pos; neg] -> 
          let a' = mk_union pos neg in 
            assert(not(Term.subterm x a'));
            let sl' = compose (x, mk_inter pos (mk_imp neg (mk_fresh()))) sl in
              solve1 a' sl'
      | _ -> failwith "Ill-formed propositional set term")
  with
      Not_found -> 
        compose (a, mk_full()) sl

and compose (x, b) sl =
  Term.Subst.compose apply (x, b) sl