sig
  type scope = int
  type 'a scoped = 'a * LogtkSubsts.scope
  type term = LogtkScopedTerm.t
  module Renaming :
    sig
      type t
      val create : unit -> LogtkSubsts.Renaming.t
      val clear : LogtkSubsts.Renaming.t -> unit
    end
  type t
  type subst = LogtkSubsts.t
  val empty : LogtkSubsts.t
  val is_empty : LogtkSubsts.t -> bool
  val lookup :
    LogtkSubsts.t ->
    LogtkSubsts.term ->
    LogtkSubsts.scope -> LogtkSubsts.term * LogtkSubsts.scope
  val get_var :
    LogtkSubsts.t ->
    LogtkSubsts.term ->
    LogtkSubsts.scope -> LogtkSubsts.term * LogtkSubsts.scope
  val mem : LogtkSubsts.t -> LogtkSubsts.term -> LogtkSubsts.scope -> bool
  exception KindError
  val bind :
    LogtkSubsts.t ->
    LogtkSubsts.term ->
    LogtkSubsts.scope ->
    LogtkSubsts.term -> LogtkSubsts.scope -> LogtkSubsts.t
  val append : LogtkSubsts.t -> LogtkSubsts.t -> LogtkSubsts.t
  val remove : LogtkSubsts.t -> LogtkSubsts.term -> int -> LogtkSubsts.t
  val domain :
    LogtkSubsts.t -> (LogtkSubsts.term * LogtkSubsts.scope) Sequence.t
  val codomain :
    LogtkSubsts.t -> (LogtkSubsts.term * LogtkSubsts.scope) Sequence.t
  val introduced :
    LogtkSubsts.t -> (LogtkSubsts.term * LogtkSubsts.scope) Sequence.t
  val is_renaming : LogtkSubsts.t -> bool
  val pp : Buffer.t -> t -> unit
  val to_string : t -> string
  val fmt : Format.formatter -> t -> unit
  val fold :
    LogtkSubsts.t ->
    '->
    ('->
     LogtkSubsts.term ->
     LogtkSubsts.scope -> LogtkSubsts.term -> LogtkSubsts.scope -> 'a) ->
    'a
  val iter :
    LogtkSubsts.t ->
    (LogtkSubsts.term ->
     LogtkSubsts.scope -> LogtkSubsts.term -> LogtkSubsts.scope -> unit) ->
    unit
  val to_seq :
    LogtkSubsts.t ->
    (LogtkSubsts.term * LogtkSubsts.scope * LogtkSubsts.term *
     LogtkSubsts.scope)
    Sequence.t
  val to_list :
    LogtkSubsts.t ->
    (LogtkSubsts.term * LogtkSubsts.scope * LogtkSubsts.term *
     LogtkSubsts.scope)
    list
  val of_seq :
    ?init:LogtkSubsts.t ->
    (LogtkSubsts.term * LogtkSubsts.scope * LogtkSubsts.term *
     LogtkSubsts.scope)
    Sequence.t -> LogtkSubsts.t
  val of_list :
    ?init:LogtkSubsts.t ->
    (LogtkSubsts.term * LogtkSubsts.scope * LogtkSubsts.term *
     LogtkSubsts.scope)
    list -> LogtkSubsts.t
  val apply :
    LogtkSubsts.t ->
    renaming:LogtkSubsts.Renaming.t ->
    LogtkSubsts.term -> LogtkSubsts.scope -> LogtkSubsts.term
  val apply_no_renaming :
    LogtkSubsts.t ->
    LogtkSubsts.term -> LogtkSubsts.scope -> LogtkSubsts.term
  module type SPECIALIZED =
    sig
      type term
      type t = LogtkSubsts.subst
      val mem :
        LogtkSubsts.SPECIALIZED.t ->
        LogtkSubsts.SPECIALIZED.term -> LogtkSubsts.scope -> bool
      val apply :
        LogtkSubsts.SPECIALIZED.t ->
        renaming:LogtkSubsts.Renaming.t ->
        LogtkSubsts.SPECIALIZED.term ->
        LogtkSubsts.scope -> LogtkSubsts.SPECIALIZED.term
      val apply_no_renaming :
        LogtkSubsts.SPECIALIZED.t ->
        LogtkSubsts.SPECIALIZED.term ->
        LogtkSubsts.scope -> LogtkSubsts.SPECIALIZED.term
      val bind :
        LogtkSubsts.SPECIALIZED.t ->
        LogtkSubsts.SPECIALIZED.term ->
        LogtkSubsts.scope ->
        LogtkSubsts.SPECIALIZED.term ->
        LogtkSubsts.scope -> LogtkSubsts.SPECIALIZED.t
    end
  module Ty :
    sig
      type term = LogtkType.t
      type t = subst
      val mem : t -> term -> scope -> bool
      val apply : t -> renaming:Renaming.t -> term -> scope -> term
      val apply_no_renaming : t -> term -> scope -> term
      val bind : t -> term -> scope -> term -> scope -> t
    end
  module FO :
    sig
      type term = LogtkFOTerm.t
      type t = subst
      val mem : t -> term -> scope -> bool
      val apply : t -> renaming:Renaming.t -> term -> scope -> term
      val apply_no_renaming : t -> term -> scope -> term
      val bind : t -> term -> scope -> term -> scope -> t
    end
  module HO :
    sig
      type term = LogtkHOTerm.t
      type t = subst
      val mem : t -> term -> scope -> bool
      val apply : t -> renaming:Renaming.t -> term -> scope -> term
      val apply_no_renaming : t -> term -> scope -> term
      val bind : t -> term -> scope -> term -> scope -> t
    end
  module Form :
    sig
      type term = LogtkFormula.FO.t
      type t = subst
      val mem : t -> term -> scope -> bool
      val apply : t -> renaming:Renaming.t -> term -> scope -> term
      val apply_no_renaming : t -> term -> scope -> term
      val bind : t -> term -> scope -> term -> scope -> t
    end
end