WIP: Give sufficient condition on cameras for swapping ▷ with implication →, wand -*, and basic updates |==>

Idea from @robbertkrebbers. Worth a review now — some failed experiments are in, since we might not have given up on them yet.

Oversimplifying, to prove the swap law for uniform predicates, we need a CMRA axiom way to turn an n-valid resource z into a z' valid at n+1 which is "close enough" to z, for some ad-hoc value of z as needed by the proof. The CMRA axiom is more complex, and proving it for gmap requires a stronger statement than what I needed to prove the swap law.

Yet, this axiom can be proved for agreement, exclusive and discrete cameras, and lifts through ofe_fun, option, products and gmap. This is more than enough for saved propositions and for heaps.

For the authoritative camera on non-discrete arguments, attempts at a proof become pretty hairy (it's not clear this should hold). However, this is necessary for the invariant camera! I'll try this again.

OTOH, if I used a standard WP (rather than a simplified version), I'd probably need more powerful swap lemmas, so YMMV.