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 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
iris/iris!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

Prove stepping (i.e., non-value) version of `atomic_wp_seq`.

See merge request iris/iris!402

Prove `Laterable (∃ x, Φ x)`.

See merge request iris/iris!401

Add VS code to the editor.md docs

See merge request iris/iris!397

Make `iAssumption` work on `⊢ ...` premises in the Coq context.

See merge request iris/iris!398

- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in `iAssumption`, which caused the error not
  to be propagated properly.

Use apply: for pair_core_id

Closes #255

See merge request iris/iris!395

mention that masks in Coq are a bit different than on paper

Closes #211

See merge request iris/iris!394