Infrastructure for the `monPred_all` modality
If everything in the context is objective, then we should be able to introduce the monPred_all modality. This should reuse the infrastructure of iAlways.
However, I would like to go a bit further: Actually, in the case everything in the context is objective, and the goal is objective too, we might want to switch to Iris proofmode to get rid of embeddings and all that.