Done with a script by Tej; see
iris/iris!609 for details.

This reverts commit 71a1fbf0, reversing
changes made to ce12f3a6.

That is, `big_sepL2_intuitionistically_forall`, `big_sepL2_forall`, and
`big_sepM2_intuitionistically_forall`.

That is, `big_sepMS_intuitionistically_forall`, `big_sepMS_forall`,
`big_sepMS_impl`, and `big_sepMS_dup`.

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.'
```

- Renamed them from `_forall` into `_gen_proper`, to avoid confusion
  with `big_sep{L,M,S,MS}_forall`, which are actually about `∀`.
- For lists and maps there now two variants, `_gen_proper_2`, in case
  the maps or lists on both sides are different, and `_gen_proper`,
  in case the maps or lists on both sides are the same.

The general idea is to first import/export modules which are further
than the current one, and then import/export modules which are close
dependencies.

This commit tries to use the same order of imports for every file, and
describes the convention in ProofGuide.md. There is one exception,
where we do not follow said convention: in program_logic/weakestpre.v,
using that order would break printing of texan triples (??).