sig
  val of_term : Wp.Lang.F.term -> Wp.Definitions.trigger
  val of_pred : Wp.Lang.F.pred -> Wp.Definitions.trigger
  val vars : Wp.Definitions.trigger -> Wp.Lang.F.Vars.t
end