sig
  type ty = Type.t
  type term = FOTerm.t
  val bind :
    Unif_intf.subst -> ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.subst
  val unification :
    ?subst:Unif_intf.subst ->
    term Scoped.t -> term Scoped.t -> Unif_intf.subst
  val matching :
    ?subst:Unif_intf.subst ->
    pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
  val matching_same_scope :
    ?protect:ty HVar.t Sequence.t ->
    ?subst:Unif_intf.subst ->
    scope:int -> pattern:term -> term -> Unif_intf.subst
  val matching_adapt_scope :
    ?protect:ty HVar.t Sequence.t ->
    ?subst:Unif_intf.subst ->
    pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
  val variant :
    ?subst:Unif_intf.subst ->
    term Scoped.t -> term Scoped.t -> Unif_intf.subst
  val equal : subst:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> bool
  val are_unifiable : term -> term -> bool
  val matches : pattern:term -> term -> bool
  val are_variant : term -> term -> bool
end