Add a general constructor from an affine BI
In master, there is a nice correspondence between the proofs in primitive.v
and the rules in the appendix. We should try to maintain such a correspondence. Currently, upred.v
proofs things in the model that can be derived, and just claims them to be (ADMISSIBLE)
in a comment.
I see two ways to achieve that:
- We could provide a general way to construct a
BiMixin
from a proof of all the laws given in the appendix. - We could do the more specific thing and first prove the appendix laws for
uPred
, and subsequently not useunseal
when proving theBiMixin
.