Modify adequacy proof to not break the 'fancy update' abstraction.

The current proof of adequacy in the master branch unfolds the definition of fancy updates and threads through a world assertion explicitly. In contrast, for the basic and later modalities there is a base logic soundness theorem, which lets one treat those modalities as a black box for purposes of proving adequacy. This is exploited very nicely in the Iris From the Ground Up paper's proof of Theorem 6, which demonstrates adequacy for a simplified version of weakest precondition without fancy updates.

@robbertkrebbers suggested to me that it might be possible to develop a fancy update soundness theorem so as to prove full adequacy in a similar way. This merge request works this out.