`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.

Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

See merge request iris/iris!414

They follow the pattern of `wp_wand`.

Kill `{o,r,ur}Functor_diag` coercions, and rename into `{o,r,ur}Functor_apply`

Closes #240

See merge request iris/iris!413

Add notion of isomorphism between OFEs

See merge request iris/iris!410

Revise uses of `inj` from !408 as discussed

See merge request iris/iris!412

Replace explicit use of Inj instances by inj

See merge request iris/iris!408

Same rationale as iris/stdpp!132.

drop_insert -> drop_insert_gt

See merge request iris/iris!407

Add missing `Proof.` to sealing proofs to help async proof checking

See merge request iris/iris!406

This helps async proof checking (see
!406 (comment 46759)).

Done with
```
gsed -i 's/seal \(.*\)\. by eexists. Qed./seal \1. Proof. by eexists. Qed./' \
  $(find theories/ -name '*.v')
```

And checked by inspecting the output of:
```
git grep '\bseal\b'|fgrep -v 'Proof. by eexists. Qed.'
```

Spell check proof_guide.md

See merge request iris/iris!405

sbi_internal_eq: add "sections" of notation, following stdpp

See merge request iris/iris!404