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
BiMixinfrom 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 use
unsealwhen proving the