sig
  type term = TermInner.Default.t
  type dt = (Model.DT_util.term, Model.DT_util.term) Model.DT.t
  type subst = (Model.DT_util.term, Model.DT_util.term) Var.Subst.t
  val ite :
    Model.DT_util.term Var.t ->
    then_:Model.DT_util.dt -> else_:Model.DT_util.dt -> Model.DT_util.dt
  val eval_subst :
    subst:Model.DT_util.subst -> Model.DT_util.dt -> Model.DT_util.dt
  val map_vars :
    subst:(Model.DT_util.term, Model.DT_util.term Var.t) Var.Subst.t ->
    Model.DT_util.dt -> Model.DT_util.dt
  val rename_vars : Model.DT_util.dt -> Model.DT_util.dt
  val apply : Model.DT_util.dt -> Model.DT_util.term -> Model.DT_util.dt
  val apply_l :
    Model.DT_util.dt -> Model.DT_util.term list -> Model.DT_util.dt
  val join : Model.DT_util.dt -> Model.DT_util.dt -> Model.DT_util.dt
  val merge : Model.DT_util.dt -> Model.DT_util.dt -> Model.DT_util.dt
  val merge_l : Model.DT_util.dt list -> Model.DT_util.dt
  val reorder :
    Model.DT_util.term Var.t list -> Model.DT_util.dt -> Model.DT_util.dt
  val remove_vars :
    Model.DT_util.term Var.t list -> Model.DT_util.dt -> Model.DT_util.dt
  val remove_first_var : Model.DT_util.dt -> Model.DT_util.dt
  exception Case_not_found of Model.DT_util.term
  val find_cases :
    ?subst:Model.DT_util.subst ->
    Model.DT_util.term ->
    (Model.DT_util.term, Model.DT_util.term) Model.DT.cases ->
    Model.DT_util.subst * Model.DT_util.dt
  val to_term : Model.DT_util.dt -> Model.DT_util.term
  val print : Model.DT_util.dt Model.printer
end