In https://github.com/coq/coq/pull/13882 it was discovered that rewrite ... in H * behaves really strangely in some cases: it implicitly revert H! This adjusts our code to not rely on that behavior any more (at least in this instance, there might be others).