Turn `internal_eq_entails` into a bi-implication

See merge request iris/iris!898

Make `unseal` tactics type-directed

See merge request iris/iris!778

Fix typo in appendix

See merge request iris/iris!895

Also, refactor the file so that all type class + canonical structure instances
are at the same place, instead of spread through the file.

Move definitions and lemmas about heap_lang locations to module `Loc`

See merge request iris/iris!890

Improve iCombine to allow a 'gives' clause for validity properties

Closes #460

See merge request iris/iris!872

Rename `f_contractive_core` into `dist_later_intro`.

See merge request iris/iris!896

Change definition of dist_later for compatability with Transfinite Iris

See merge request iris/iris!886

Prove that invariants are "except 0".

See merge request iris/iris!897

Some instances of tau should have been tau'

In logatom lock: Formalize that the lock is Free before acquire.

See merge request iris/iris!891

Adapt to https://github.com/coq/coq/pull/16788

See merge request iris/iris!893

add big_opM_gset_to_gmap

See merge request iris/iris!878