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

fix Coq 8.18 deprecation warnings

See merge request iris/iris!986

drop support for Coq 8.15

See merge request iris/iris!985