Lemmas about updates should be instantiated by default witht the current BI instead of `iProp`

The instances for the FUpd and FUpdFacts type classes are set in a way that gives the priority to iProp? Therefore, when using lemmas about updates in vProp, we sometimes have to manually instantiate them with the current BI. Otherwise, the lemmas are instantiated with iProp and used through the embedding.

See, for example https://gitlab.mpi-sws.org/FP/sra-gps/blob/gen_proofmode_WIP/theories/examples/circ_buffer.v#L236

The instances for the AsValid type class prioritizes the fact of not using the embedding, so we should be able to fix this issue by simply making sure the search for AsValid occurs before FUpd, but I do not know how to do that.

@robbertkrebbers, any idea?