Draft: Staging MR for various refactorings

It turns out that properly fixing !507 (closed) opened quite a can of worms. We have the following related MRs now:

• !526 (merged)
• !530
• !531 (merged)
• non_empty change as discussed in !526 (comment 97794)
• Direction of equality in fmap/omap/alter lemmas, see !531 (comment 97789)

The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.