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