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")

The new adequacy statement unifies `wp_strong_adequacy`, `wp_strong_all_adequacy`,
and `wp_invariance`.

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.

This is in preparation for coq/coq#9274.

Thanks @jtassaro.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

This commit extends the state interpretation with an additional parameter to
talk about the number of forked-off threads, and a fixed postcondition for each
forked-off thread:

    state_interp : Λstate → list Λobservation → nat → iProp Σ;
    fork_post : iProp Σ;

This way, instead of having `True` as the post-condition of `Fork`, one can
have any post-condition, which is then recorded in the state interpretation.
The point of keeping track of the postconditions of forked-off threads, is that
we get an (additional) stronger adequacy theorem:

    Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
       (∀ `{Hinv : invG Σ} κs,
         (|={⊤}=> ∃
             (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
             (fork_post : iProp Σ),
           let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
           stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
             let m := length vs in
             stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
      rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
      φ v.

The difference with the ordinary adequacy theorem is that this one only applies
once all threads terminated. In this case, one gets back the post-conditions
`[∗] replicate m fork_post` of all forked-off threads.

In Iron we showed that we can use this mechanism to make sure that all
resources are disposed of properly in the presence of fork-based concurrency.