Add a Strategy command for ucmra and cmra projections

Investigate timing consequences of adding a Strategy command. Motivation was the following example:

From iris.algebra Require Import frac_auth agree numbers auth.
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Import proofmode.

Strategy expand [ucmra_cmraR ucmra_equiv ucmra_dist ucmra_pcore ucmra_op ucmra_valid ucmra_validN ucmra_ofe_mixin ucmra_cmra_mixin].

Section weird_slow_qed.               (* using UR here *)
  Lemma slow_qed `{!inG Σ (frac_authUR $ optionUR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (Some $ to_agree n)) ⊢ own γ1 (●F (Some $ to_agree n)).
  Proof. time iIntros "$". Time Qed. (* 0.2 seconds -> now 0.01 *)

                                      (* using R here *)
  Lemma fast_qed `{!inG Σ (frac_authUR $ optionR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (Some $ to_agree n)) ⊢ own γ1 (●F (Some $ to_agree n)).
  Proof. time iIntros "$". Time Qed. (* instant *)

                                      (* using UR here *)
  Lemma slow_qed2 `{!inG Σ (frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (●F (to_agree n))) ⊢ own γ1 (●F (●F (to_agree n))).
  Proof. time iIntros "$". Time Qed. (* 1.4 seconds! -> now 0.044 *)

                                       (* using R here *)
  Lemma fast_qed2 `{!inG Σ (frac_authUR $ frac_authR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (●F (to_agree n))) ⊢ own γ1 (●F (●F (to_agree n))).
  Proof. time iIntros "$". Time Qed. (* instant *)

  (* Note that if proven with `reflexivity`, Qed also becomes instant *)
End weird_slow_qed.

where Strategy offers a drastic performance improvement.