Add more primitive projections

This merge request adds more primitive projections to various parts of Iris. The result should be some performance improvements, because the size of proof terms decreases. For example, see this comparison of Iris Examples builds where in the faster build primitive projections are enabled for the various extensions of bi (e.g., updates).