Take a closer look at the interaction of fancy updates and plainly
Currently we have these two laws:
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} :
(▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
First, I find it surprising that we need two laws. Second, the first law looks really unwieldy.