sig
  type t
  type scope = int
  type renaming
  val empty : TopDown.S.Subst.t
  val bind :
    TopDown.S.Subst.t ->
    TopDown.S.T.t ->
    TopDown.S.Subst.scope ->
    TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.Subst.t
  val deref :
    TopDown.S.Subst.t ->
    TopDown.S.T.t ->
    TopDown.S.Subst.scope -> TopDown.S.T.t * TopDown.S.Subst.scope
  val create_renaming : unit -> TopDown.S.Subst.renaming
  val reset_renaming : TopDown.S.Subst.renaming -> unit
  val rename :
    renaming:TopDown.S.Subst.renaming ->
    TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
  val eval :
    TopDown.S.Subst.t ->
    renaming:TopDown.S.Subst.renaming ->
    TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
  val eval_lit :
    TopDown.S.Subst.t ->
    renaming:TopDown.S.Subst.renaming ->
    TopDown.S.Lit.t -> TopDown.S.Subst.scope -> TopDown.S.Lit.t
  val eval_lits :
    TopDown.S.Subst.t ->
    renaming:TopDown.S.Subst.renaming ->
    TopDown.S.Lit.t list -> TopDown.S.Subst.scope -> TopDown.S.Lit.t list
  val eval_clause :
    TopDown.S.Subst.t ->
    renaming:TopDown.S.Subst.renaming ->
    TopDown.S.C.t -> TopDown.S.Subst.scope -> TopDown.S.C.t
end