Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse
the type of the term and generate goals for the premises, we repeatedly
apply a series of lemmas. This has the advantage that it works up to
convertability, and we no longer need the `eval ...` hacks.

There is no need to include the `(∃ P', □ ▷ (P  P')  ...` since we
get closure under `▷ □ ` from regular invariants.

Due to the new semantic invariants (!319) we no longer need to
close the model (i.e. `inv_def`) to be contractive, the semantic
invariant definition (i.e. `inv`) is already contractive.

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 (??).

Turn all `f_op` lemmas to have shape `f (x ⋅ y) = f x ⋅ f y`, following the plan
in iris/iris!295 (comment 39151), plus
`cmra_morphism_op`.

Used the following script:

sed '
s/\bCofeMor/OfeMor/g;
s/\-c>/\-d>/g;
s/\bcFunctor/oFunctor/g;
s/\bCFunctor/OFunctor/g;
s/\b\%CF/\%OF/g;
s/\bconstCF/constOF/g;
s/\bidCF/idOF/g
s/\bdiscreteC/discreteO/g;
s/\bleibnizC/leibnizO/g;
s/\bunitC/unitO/g;
s/\bprodC/prodO/g;
s/\bsumC/sumO/g;
s/\bboolC/boolO/g;
s/\bnatC/natO/g;
s/\bpositiveC/positiveO/g;
s/\bNC/NO/g;
s/\bZC/ZO/g;
s/\boptionC/optionO/g;
s/\blaterC/laterO/g;
s/\bofe\_fun/discrete\_fun/g;
s/\bdiscrete\_funC/discrete\_funO/g;
s/\bofe\_morC/ofe\_morO/g;
s/\bsigC/sigO/g;
s/\buPredC/uPredO/g;
s/\bcsumC/csumO/g;
s/\bagreeC/agreeO/g;
s/\bauthC/authO/g;
s/\bnamespace_mapC/namespace\_mapO/g;
s/\bcmra\_ofeC/cmra\_ofeO/g;
s/\bucmra\_ofeC/ucmra\_ofeO/g;
s/\bexclC/exclO/g;
s/\bgmapC/gmapO/g;
s/\blistC/listO/g;
s/\bvecC/vecO/g;
s/\bgsetC/gsetO/g;
s/\bgset\_disjC/gset\_disjO/g;
s/\bcoPsetC/coPsetO/g;
s/\bgmultisetC/gmultisetO/g;
s/\bufracC/ufracO/g
s/\bfracC/fracO/g;
s/\bvalidityC/validityO/g;
s/\bbi\_ofeC/bi\_ofeO/g;
s/\bsbi\_ofeC/sbi\_ofeO/g;
s/\bmonPredC/monPredO/g;
s/\bstateC/stateO/g;
s/\bvalC/valO/g;
s/\bexprC/exprO/g;
s/\blocC/locO/g;
' -i $(find theories -name "*.v")

This allows one to make use of recursive ghost state obtained from the
recursive domain equation solver.

With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like

> looking for (subG
>                       (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
>                          ?cFunctorContractive0) Σ)

This MR is a follow up on the renamings performed (implicitly) as part of
!215. This MR makes the following changes:

- `auth_both_frac_valid` and `auth_both_valid` are now of the same shape
  as `auth_both_frac_validN` and `auth_both_validN`. That is, both are
  now biimplications.
- The left-to-right  direction of `auth_both_frac_valid` and
  `auth_both_valid` only holds in case the camera is discrete. The
  right-to-left versions for non-discrete cameras are prefixed `_2`, the
  convention that we use throughout the development.
- Change the direction of lemmas like `auth_frag_valid` and
  `auth_auth_valid` so that it's consistent with the other lemmas. I.e.
  make sure that the ◯ and ● are always on the LHS of the biimplication.

Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version
of the same lemma. I favored the `big_opL_op` naming scheme.