The view camera.

This MR implements #257 (closed): a view camera that generalize authoritative camera. The camera view A B rel is parametrized by an OFE A for the authoritative elements, a camera B for the fragments, and a step-indexed relation rel that relates the two.

To show that the view camera indeed generalizes the authoritative camera, I have implemented the authoritative camera auth in terms of the view camera. The new implementation is pretty much a drop-in replacement, as shown by that fact that the whole of Iris compiles without any changes.

Some notes:

• I have defined the laws for the view relation using a canonical structure instead of a type class. My experience is that parameterizing a canonical structure (in this case, the camera instance for view) by a type class is pretty unreliable.
• I removed a bunch of lemmas about auth that break the abstraction of ●/◯ and used the Auth constructor directly. This will likely cause some breakage in reverse dependencies, but I'm happy to fix that.
• I still need to write a bunch of documentation (as comments). I will do this after some initial feedback.

TODOs for future MRs:

• Define the heap/gmap camera (!486 (merged)) in terms of the view camera and the discardable fractions camera (!497 (merged)).
• Define the camera for monotone partial bijections (!91 (closed)) in terms of the view camera.
• Develop a theory of local updates for the view camera. Currently there are just lemmas like view_update that use the view relation directly in the premise. The current lemmas are sufficient to prove the local update lemmas for auth.
• Define the view relation in terms of siProp. To do this, it makes sense to first define validity ✓, inclusion ≼, etc, as siProps, otherwise there is little point to that.
• Investigate sealing the view/auth definitions. It's often the case (already prior to the MR) that Coq loops if you apply the wrong auth lemma. Sealing might fix that.