module Filtering:sig
..end
true
when ~polarity:false
(for hypotheses)false
when ~polarity:true
(for goals)filter ~polarity:true f p ==> p
p ==> filter ~polarity:false f p
theory/filtering.why
for proofs.val filter : polarity:bool -> (Lang.F.pred -> bool) -> Lang.F.pred -> Lang.F.pred
val compute : ?anti:bool -> Conditions.sequent -> Conditions.sequent