sig
  type t
  val equal : Letify.??.t -> Letify.??.t -> bool
  val pretty : string -> Format.formatter -> Letify.??.t -> unit
  val empty : Letify.??.t
  val add : Lang.F.var -> Lang.F.term -> Letify.??.t -> Letify.??.t
  val mem : Lang.F.var -> Letify.??.t -> bool
  val find : Lang.F.var -> Letify.??.t -> Lang.F.term
  val e_apply : Letify.??.t -> Lang.F.term -> Lang.F.term
  val p_apply : Letify.??.t -> Lang.F.pred -> Lang.F.pred
  val assume : Letify.??.t -> Lang.F.pred -> Letify.??.t
  val iter : (Lang.F.var -> Lang.F.term -> unit) -> Letify.??.t -> unit
  val class_of : Letify.??.t -> Lang.F.var -> Lang.F.var list
  val domain : Letify.??.t -> Lang.F.Vars.t
  val codomain : Letify.??.t -> Lang.F.Vars.t
end