In some cases, destruct H won't be able to clear H from the context. This causes straightline to get stuck in a loop, trying to destruct the same hypothesis on each iteration. This change ensures that we only call destruct H when we know that this won't happen.
In some cases,
destruct Hwon't be able to clear H from the context. This causesstraightlineto get stuck in a loop, trying to destruct the same hypothesis on each iteration. This change ensures that we only calldestruct Hwhen we know that this won't happen.