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