diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 8ae2868442822f026dfb6fffe0a705a9a6afb215..55bb86317a9b22f07812f5c9959cc41c7d7dca06 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -470,28 +470,6 @@ Lemma authO_map_ne A B : NonExpansive (@authO_map A B).
 Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
   apply agreeO_map_ne; auto. Qed.
 
-Program Definition authRF (F : urFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
-Qed.
-Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
-Qed.
-Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
-  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
-Qed.
-
-Instance authRF_contractive F :
-  urFunctorContractive F → rFunctorContractive (authRF F).
-Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
-Qed.
-
 Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
@@ -513,3 +491,6 @@ Instance authURF_contractive F :
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
+
+Definition authRF (F : urFunctor) :=
+  urFunctor_to_rFunctor (authURF F).
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 53b4b850d178a64b38dfc5863aadf5c6f4e1de8c..cc934383eb0eea941e2d1051517f193839678b92 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -817,6 +817,12 @@ Next Obligation.
   apply rFunctor_map_compose.
 Qed.
 
+Global Instance rFunctor_to_oFunctor_contractive F :
+  rFunctorContractive F → oFunctorContractive (rFunctor_to_oFunctor F).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply rFunctor_map_contractive. done.
+Qed.
+
 Program Definition rFunctor_oFunctor_compose (F1 : rFunctor) (F2 : oFunctor)
   `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
   rFunctor_car A _ B _ := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
@@ -902,6 +908,12 @@ Next Obligation.
   apply urFunctor_map_compose.
 Qed.
 
+Global Instance urFunctor_to_rFunctor_contractive F :
+  urFunctorContractive F → rFunctorContractive (urFunctor_to_rFunctor F).
+Proof.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply urFunctor_map_contractive. done.
+Qed.
+
 Program Definition urFunctor_oFunctor_compose (F1 : urFunctor) (F2 : oFunctor)
   `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
   urFunctor_car A _ B _ := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
@@ -1526,28 +1538,6 @@ Proof.
   - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
 Qed.
 
-Program Definition optionRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
-Qed.
-Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
-Qed.
-Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
-Qed.
-
-Instance optionRF_contractive F :
-  rFunctorContractive F → rFunctorContractive (optionRF F).
-Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
-Qed.
-
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
@@ -1570,6 +1560,9 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
+Definition optionRF (F : rFunctor) : rFunctor :=
+  urFunctor_to_rFunctor (optionURF F).
+
 (* Dependently-typed functions over a discrete domain *)
 Section discrete_fun_cmra.
   Context `{B : A → ucmraT}.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 025d04df0abc776542b0c0be4d3daf63abe2dce7..8e02356eec397d09dbab063a50f04b541fb0c459 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -675,11 +675,11 @@ Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
 Qed.
-Instance gmapRF_contractive K `{Countable K} F :
+Instance gmapURF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
 Qed.
 
 Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor :=
-  urFunctor_to_rFunctor $ gmapURF K F.
+  urFunctor_to_rFunctor (gmapURF K F).
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index d1f9f0c3bdd5e74929a5c32f90ca6add88e3f82a..4e9fcf61f69ca8e77a1a3beab7c3b08654ec98b6 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -573,4 +573,4 @@ Proof.
 Qed.
 
 Definition listRF (F : urFunctor) : rFunctor :=
-  urFunctor_to_rFunctor $ listURF F.
+  urFunctor_to_rFunctor (listURF F).