Previously, each individual instance in the option OFE and camera
instances (i.e. `Dist`, `Valid`, etc.) required a full OFE (resp.
camera) instance for the argument type of the option. This makes using
option in the definition of recursively-defined OFEs and cameras
annoyingly hard, since you can't use e.g. the option `Dist` to define
your recursive `Dist` instance, since your type isn't yet an OFE.

This change strengthens all these instances to just require an instance
of the same class on the argument type, so that they can be relied on for
implementing an OFE. Ideally all the lemmas associated with these
instances would also be strengthened, but these are harder to
generalise, so I've opted to skip over that work for now.

Release 4.1.0

See merge request iris/iris!1003

Streamline "inversion" lemmas for `dist` on `list`

See merge request iris/iris!1002

Lemmas and instances for `∪` on `gmap`.

See merge request iris/iris!998

`Inj`/`Forall2` results for `list`/`option` similar to std++.

See merge request iris/iris!999

This is an outstanding TODO from iris/stdpp!496

add option_fmap_dist_inj lemma

See merge request iris/iris!969

Rename instances `union_with_proper` → `union_with_ne`, ...

See merge request iris/iris!997

Add lemma `later_map_Next`.

See merge request iris/iris!996

Add instance `cons_dist_inj`.

See merge request iris/iris!995

`map_fmap_proper` → `map_fmap_ne`, `map_zip_with_proper` → `map_zip_with_ne`.

Remove useless `BiAffine` conditions for big op `Plain` instances.

See merge request iris/iris!994

String_ident tweaks

See merge request iris/iris!993

Document convention to use `f_as_g` in naming.

See merge request iris/iris!990

See iris/stdpp!459 (comment 96622)

logically atomic triples: add private postcondition

Closes #473

See merge request iris/iris!956

Naming convention about lookup/elem_of.

See merge request iris/iris!988

remove some Coq 8.15 support hacks

See merge request iris/iris!987