add better lemmas for working with mask-changing fupd, and rearrange names a bit

A proposal for addressing parts of !527 (closed) and !615 (closed) without adding any new proofmode typeclass instances.

The heart of this MR are two new lemmas that can be conveniently iApplyed when having a mask-changing fupd as the goal:

  (** Weaken the first mask of the goal from [E1] to [E2].
      This lemma is intended to be [iApply]ed. *)
  Lemma fupd_mask_weaken {E1} E2 {E3 P} :
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) ={E2,E3}=∗ P) -∗ |={E1,E3}=> P.
  (** Introduction lemma for a mask-changing fupd.
      This lemma is intended to be [iApply]ed. *)
  Lemma fupd_mask_intro E1 E2 P:
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) -∗ P) -∗ |={E1,E2}=> P.

In particular the second lemma is easier to use than the old fupd_mask_intro' that was used for both the "weaken" and the "intro" case. For the "weaken" case, I think fupd_mask_intro', with some adjustment to the implicit parameters, is still the better choice, so that's what this MR proposes.

Sadly, fupd_mask_weaken is already taken as a name, and so is fupd_intro_mask which is way too confusing when adding fupd_mask_intro. So this MR also renames some existing lemmas: fupd_intro_mask → fupd_mask_intro_subseteq, fupd_intro_mask' → fupd_mask_subseteq, fupd_mask_weaken → fupd_mask_intro_discard. Finally, it removes the unused fupd_mask_same.

We now have fupd_mask_subseteq in the fupd typeclass instead of the more general fupd_mask_intro_subseteq; the latter can be derived from the former.

All of these lemmas involve a subseteq but only some have it in the name -- so the names aren't really great, but I also feel like we reached a local maximum here.