sig
  type t = [ `Exists | `Forall | `Fun | `Mu ]
  val lift : TermMono.Binder.t -> TI.Binder.t
end