better support for view shift with mismatching masks

This adds better support for using view shifts when the mask does not match the goal. Fixes #31.

Usually the easiest way to handle such a situation is to use fupd_intro_mask', but that is hard to discover and also hard to use without repeating the masks. So with this MR, the goal is to replace that lemma by something better. There are actually two ways the lemma gets used:

• It is used to iMod a view shift whose first mask does not match the first mask of the goal. For this I added a new low-priority ElimModal instance. It is a somewhat odd instance because the assertion that "comes out" of it is ((|={E1',E1}=> emp) ∗ P) where P is the conclusion of the eliminated view shift, but this still seems way more convenient and easier to discover than having to iApply a lemma.
• The lemma is also used to iModIntro when the view shift is still mask-changing. I found no good way to do anything automatic here though, so I just made a lemma that is easier to use for this purpose, fupd_intro_mask_adjust. (A better name might be fupd_intro_mask but that name is already used.)

This is not the most general way to handle mask mismatches, in particular for the iMod part. fupd_mask_frame encodes the most general way. But that requires reasoning about "interesting" (in)equalities of masks, some of which even have to exploit that mask membership is decidable. The only user of fupd_mask_frame that I know of is fupd_mask_frame_acc, an even more complicated lemma for handling mask mismatches, which in turn is used for atomic_acc_mask, which is a cute fact about atomic accessors that I am happy to know is true but which is never actually used. No Iris reverse dependency that we track on CI uses fupd_mask_frame or fupd_mask_frame_acc, but fupd_intro_mask' has quite a few users. So given that it seems fine for me that iMod would do something less general that is good enough for basically everything we saw so far.

@robbertkrebbers @tchajed what do you think?