sig
  val pp_print_model : Format.formatter -> (Var.t * Term.t) list -> unit
  val eliminate : Model.t -> Var.t list -> Poly.cformula -> Poly.cformula
end