Implement monotone partial bijections as a view
This is an alternative to !91 (closed), which was written prior to views. Using the view CMRA we factor the implementation into purely algebraic library and a logic-level wrapper. The logic-level wrapper exports resources which seal away the underlying ownership and has theorems which handle the ownership reasoning.
CC @dfrumin (author of !91 (closed)) and @amintimany who were using a library like this in runST and iris-logrel.
One thing I tried to do here is write the motivation for the library, as a comment in the logic-level own_bij.v library. I didn't understand the point of the library until @jung explained it to me.