A binary feature that returns zero iff the constraint of the given taclet app
is stronger than the original constraint of the formula to which the rule is
applied (i.e. replacewith-clauses are changed into add-clauses). For taclets
that do not have a find-clause, the app constraint is compared with the
conjunction of the constraints attached to matched if-formulas.