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?