should corres_underlying imply failure preservation?

[lsf37]

While discussing the monadic rewrite framework in #487, we realised that monadic_rewrite demands that failure on the concrete side implies failure of the abstract side. This is a general refinement principle, but it is not the case in our current definition of corres_underlying.

This is not a problem for the strength of our current refinement theorems, because corres_underlying has these failure flags that control which failures we need to prove and which we can assume, and the way we use them has the correct properties (implies absence of failure in the refinement stack).

One could still make the argument that this makes corres_underlying a bit strange in terms of refinement definitions. If it had the implication, we would get the expected standard definition of refinement when the state space of abstract and concrete are equal (i.e. just subset and failure implication). Currently, one would have to add the failure implication separately. Apart from philosophical niceness, this also has an impact on the relationship between monadic_rewrite (which does this correctly) and corres_underlying (where it is ad-hoc).

It'd be easy to change the definition, but the usual worry is that too many proofs would need to be updated. We should investigate how bad it really would be to do that.