ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite
under binders. This might incur a significant time penalty.