sig
  type term = InnerTerm.t
  type var = InnerTerm.t HVar.t
  module Renaming :
    sig
      type t
      val create : unit -> Substs.Renaming.t
      val clear : Substs.Renaming.t -> unit
    end
  type t
  type subst = Substs.t
  val empty : Substs.t
  val is_empty : Substs.t -> bool
  val find_exn : Substs.t -> Substs.var Scoped.t -> Substs.term Scoped.t
  val find : Substs.t -> Substs.var Scoped.t -> Substs.term Scoped.t option
  val deref : Substs.t -> Substs.term Scoped.t -> Substs.term Scoped.t
  val get_var :
    Substs.t -> Substs.var Scoped.t -> Substs.term Scoped.t option
  val mem : Substs.t -> Substs.var Scoped.t -> bool
  exception InconsistentBinding of Substs.var Scoped.t *
              Substs.term Scoped.t * Substs.term Scoped.t
  val bind :
    Substs.t -> Substs.var Scoped.t -> Substs.term Scoped.t -> Substs.t
  val append : Substs.t -> Substs.t -> Substs.t
  val remove : Substs.t -> Substs.var Scoped.t -> Substs.t
  val domain : Substs.t -> Substs.var Scoped.t Sequence.t
  val codomain : Substs.t -> Substs.term Scoped.t Sequence.t
  val introduced : Substs.t -> Substs.var Scoped.t Sequence.t
  val is_renaming : Substs.t -> bool
  val pp : t CCFormat.printer
  val to_string : t -> string
  val fold :
    ('a -> Substs.var Scoped.t -> Substs.term Scoped.t -> 'a) ->
    'a -> Substs.t -> 'a
  val iter :
    (Substs.var Scoped.t -> Substs.term Scoped.t -> unit) -> Substs.t -> unit
  val to_seq :
    Substs.t -> (Substs.var Scoped.t * Substs.term Scoped.t) Sequence.t
  val to_list : Substs.t -> (Substs.var Scoped.t * Substs.term Scoped.t) list
  val of_seq :
    ?init:Substs.t ->
    (Substs.var Scoped.t * Substs.term Scoped.t) Sequence.t -> Substs.t
  val of_list :
    ?init:Substs.t ->
    (Substs.var Scoped.t * Substs.term Scoped.t) list -> Substs.t
  val apply :
    Substs.t ->
    renaming:Substs.Renaming.t -> Substs.term Scoped.t -> Substs.term
  val apply_no_renaming : Substs.t -> Substs.term Scoped.t -> Substs.term
  module type SPECIALIZED =
    sig
      type term
      type t = Substs.subst
      val find_exn :
        Substs.SPECIALIZED.t ->
        Substs.var Scoped.t -> Substs.SPECIALIZED.term Scoped.t
      val get_var :
        Substs.SPECIALIZED.t ->
        Substs.var Scoped.t -> Substs.SPECIALIZED.term Scoped.t option
      val deref :
        Substs.SPECIALIZED.t ->
        Substs.SPECIALIZED.term Scoped.t -> Substs.SPECIALIZED.term Scoped.t
      val apply :
        Substs.SPECIALIZED.t ->
        renaming:Substs.Renaming.t ->
        Substs.SPECIALIZED.term Scoped.t -> Substs.SPECIALIZED.term
      val apply_no_renaming :
        Substs.SPECIALIZED.t ->
        Substs.SPECIALIZED.term Scoped.t -> Substs.SPECIALIZED.term
      val bind :
        Substs.SPECIALIZED.t ->
        Substs.var Scoped.t ->
        Substs.SPECIALIZED.term Scoped.t -> Substs.SPECIALIZED.t
    end
  module Ty :
    sig
      type term = Type.t
      type t = subst
      val find_exn : t -> var Scoped.t -> term Scoped.t
      val get_var : t -> var Scoped.t -> term Scoped.t option
      val deref : t -> term Scoped.t -> term Scoped.t
      val apply : t -> renaming:Renaming.t -> term Scoped.t -> term
      val apply_no_renaming : t -> term Scoped.t -> term
      val bind : t -> var Scoped.t -> term Scoped.t -> t
    end
  module FO :
    sig
      type term = FOTerm.t
      type t = subst
      val find_exn : t -> var Scoped.t -> term Scoped.t
      val get_var : t -> var Scoped.t -> term Scoped.t option
      val deref : t -> term Scoped.t -> term Scoped.t
      val apply : t -> renaming:Renaming.t -> term Scoped.t -> term
      val apply_no_renaming : t -> term Scoped.t -> term
      val bind : t -> var Scoped.t -> term Scoped.t -> t
    end
end