generalize gmap_view for an arbitrary CMRA as values

gmap_view is currently limited to gmap K V where V: ofe, hard-coding agree behavior for the values. This MR lifts that limitation and allows an arbitrary V: cmra. This is needed, for instance, to equip a lambda-rust/Perennial style heap (with reader-writer locks for data race modeling) with a persistent points-to based on dfrac: those heaps need a custom RA for handling the lock state, so the old gmap_view doesn't cut it.

This has the downside that existing users of gmap_view now have to do all the agreement stuff themselves, which can be somewhat painful. I tried my best to add suitable lemmas that make this as easy as possible. In particular, gmap_view_both_dfrac_valid_discrete_total synergizes well with the new to_agree_included_L.

This MR is based on !957 (merged).