Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms

An attempt to fix #539. In summary, this MR:

• makes auth a Definition, instead of a Notation
• provides better Canonical instances for seeing auth as an ofe/cmra/ucmra. Previously, those of view were used, which can result in some very large terms.
• changes the definition of ucmra to an equivalent one, which ensures that the ucmra_cmraR coercion can compute fast on nested terms.

I believe all 3 changes are necessary to fix #539:

• The first two make it feasible to Time Check (● (● (● (● (● (● (● (● (● (● (● (● (()))))))))))))).
• The last one is necessary to get problems like the following to type check quickly

Time Lemma stack_frac_auths5 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) : 
      own γ1 (●F (●F (●F (●F (●F (to_agree n)))))) ⊢ own γ1 (●F (●F (●F (●F (●F (to_agree n)))))).

It additionally reverts !907 (merged) and instead registers a strategy that prevents unfolding authR and authO. Unfolding those would reveal the underlying view structure, which may cause an exponential blow-up in unification time.

I am quite interested in the timing for this MR, also for dependencies on Iris. The changes to ucmra might break stuff elsewhere, or make stuff slower.. in which case this might not be the way to go.

Also note that this MR uses the reversible attribute, which means we need Coq 8.16.1+.