sig
  type t = Var of Var.t * int | App of Sym.t * Term.t list * int
  and trm = Term.t
  val hash : Term.t -> int
  val pp : Term.t Pretty.printer
  val to_string : Term.t -> string
  module Var :
    sig
      val mk_var : Name.t -> Var.Cnstrnt.t -> Term.t
      val k : int Pervasives.ref
      val mk_rename : Name.t -> int option -> Var.Cnstrnt.t -> Term.t
      val mk_slack : int option -> Var.slack -> Term.t
      val mk_fresh : Th.t -> int option -> Var.Cnstrnt.t -> Term.t
      val mk_const : Th.t -> int option -> Var.Cnstrnt.t -> Term.t
      val is_rename : Term.t -> bool
      val is_external : Term.t -> bool
      val is_fresh : Th.t -> Term.t -> bool
      val is_const : Term.t -> bool
      val is_slack : Term.t -> bool
      val d_external : Term.t -> Name.t * Var.Cnstrnt.t
      val is_zero_slack : Term.t -> bool
      val is_nonneg_slack : Term.t -> bool
      val is_internal : Term.t -> bool
      val is_dom : Dom.t -> Term.t -> bool
      val is_int : Term.t -> bool
      val is_real : Term.t -> bool
      val compare : Term.t -> Term.t -> int
      module Set :
        sig
          type elt = trm
          and t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
        end
      module Map :
        sig
          type key = trm
          and +'a t
          val empty : 'a t
          val add : key -> 'a -> 'a t -> 'a t
          val find : key -> 'a t -> 'a
          val remove : key -> 'a t -> 'a t
          val mem : key -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
        end
      val name_of : Term.t -> Name.t
      val dom_of : Term.t -> Dom.t
      val width_of : Term.t -> int
      val cnstrnt_of : Term.t -> Var.Cnstrnt.t
    end
  module App :
    sig
      val mk_const : Sym.t -> Term.t
      val mk_app : Sym.t -> Term.t list -> Term.t
      val destruct : Term.t -> Sym.t * Term.t list
      val sym_of : Term.t -> Sym.t
      val theory_of : Term.t -> Th.t
      val args_of : Term.t -> Term.t list
    end
  val is_var : Term.t -> bool
  val is_app : Term.t -> bool
  val is_const : Term.t -> bool
  val is_pure : Th.t -> Term.t -> bool
  type status = Variable | Pure of Th.t | Mixed of Th.t * Term.t
  val status : Term.t -> Term.status
  val is_equal : Term.t -> Term.t -> Three.t
  val eq : Term.t -> Term.t -> bool
  val eql : Term.t list -> Term.t list -> bool
  val cmp : Term.t -> Term.t -> int
  val compare : Term.t -> Term.t -> int
  val ( <<< ) : Term.t -> Term.t -> bool
  val orient : Term.t * Term.t -> Term.t * Term.t
  val fold : (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
  val iter : (Term.t -> unit) -> Term.t -> unit
  val for_all : (Term.t -> bool) -> Term.t -> bool
  val mapl : (Term.t -> Term.t) -> Term.t list -> Term.t list
  val choose : (Term.t -> bool) -> Term.t -> Term.t
  val subterm : Term.t -> Term.t -> bool
  val occurs : Term.t -> Term.t -> bool
  val assq : Term.t -> (Term.t * 'a) list -> 'a
  module Set2 :
    sig
      type elt = trm * trm
      and t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
    end
  module Set :
    sig
      type elt = trm
      and t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
    end
  module Map :
    sig
      type key = trm
      and +'a t
      val empty : 'a t
      val add : key -> 'a -> 'a t -> 'a t
      val find : key -> 'a t -> 'a
      val remove : key -> 'a t -> 'a t
      val mem : key -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
    end
  val vars_of : Term.t -> Term.Var.Set.t
  module Equal :
    sig
      type t = Term.trm * Term.trm
      val lhs : Term.Equal.t -> Term.trm
      val rhs : Term.Equal.t -> Term.trm
      val make : Term.trm * Term.trm -> Term.Equal.t
      val destruct : Term.Equal.t -> Term.trm * Term.trm
      val pp : Term.Equal.t Pretty.printer
      val compare : Term.Equal.t -> Term.Equal.t -> int
      val is_var : Term.Equal.t -> bool
      val is_pure : Th.t -> Term.Equal.t -> bool
    end
  type apply = Term.t * Term.t -> Term.t -> Term.t
  and map = (Term.t -> Term.t) -> Term.t -> Term.t
  module Subst :
    sig
      type t = (Term.trm * Term.trm) list
      val pp : Term.Subst.t Pretty.printer
      val empty : Term.Subst.t
      val fuse :
        Term.apply -> Term.trm * Term.trm -> Term.Subst.t -> Term.Subst.t
      val compose :
        Term.apply -> Term.trm * Term.trm -> Term.Subst.t -> Term.Subst.t
      val lookup : Term.Subst.t -> Term.trm -> Term.trm
      val invlookup : Term.Subst.t -> (Term.trm -> bool) -> Term.trm
      val apply :
        Term.map ->
        ((Term.trm * Term.trm) * 'a) list -> Term.trm -> Term.trm * 'a list
      val fold :
        (Term.trm * Term.trm -> 'a -> 'a) -> Term.Subst.t -> 'a -> 'a
    end
end