chore: robustify for byAsSorry (#6287)

This PR makes some proofs more robust so they will still work with
`byAsSorry`. Unfortunately, they are not a complete fix and there are
remaining problems building with `byAsSorry`.
8 files changed