> After further thought, it seems like the place to deal with this is
> really operator_predicate_proof(), as in the attached draft patch
> against HEAD. This passes the smell test for me, in the sense that
> it's an arguably correct and general extension of the proof rules,
> but it could use more testing.
I am not sure if we are covering the case when clause_const and
pred_const are both NULL. In this case, we should be able to return
true only by checking op_strict(pred_op) or maybe even without
checking that. Am I mistaken?