sig
  type t
  val create : unit -> t
  val copy : t -> t
  val clear : t -> unit
  val used : t -> string -> bool
  val fresh : t -> ?suggest:bool -> string -> string
  val define : t -> string -> Lang.F.term -> unit
  val unfold : t -> Lang.F.term -> unit
  val shared : t -> Lang.F.term -> bool
  val shareable : t -> Lang.F.term -> bool
  val lookup : t -> Lang.F.term -> Qed.Engine.scope
end