sig
  val extract :
    (UfSymbol.t * (Var.t list * Term.t)) list ->
    Model.t -> Term.t -> Term.t list * Term.t list
end