# 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 use`unseal`

when proving the`BiMixin`

.