sig
  type env = InnerTerm.t DBEnv.t
  val closed : InnerTerm.t -> bool
  val contains : InnerTerm.t -> int -> bool
  val shift : int -> InnerTerm.t -> InnerTerm.t
  val unshift : int -> InnerTerm.t -> InnerTerm.t
  val replace : InnerTerm.t -> sub:InnerTerm.t -> InnerTerm.t
  val from_var : InnerTerm.t -> var:InnerTerm.t -> InnerTerm.t
  val eval : InnerTerm.DB.env -> InnerTerm.t -> InnerTerm.t
  val apply_subst :
    InnerTerm.t InnerTerm.VarMap.t -> InnerTerm.t -> InnerTerm.t
end