sig val filter : polarity:bool -> (Wp.Lang.F.pred -> bool) -> Wp.Lang.F.pred -> Wp.Lang.F.pred val compute : ?anti:bool -> Wp.Conditions.sequent -> Wp.Conditions.sequent end