diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 6e3b7311afb29d4aa687e015c12eee757be176f4..025d04df0abc776542b0c0be4d3daf63abe2dce7 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -680,3 +680,6 @@ Instance gmapRF_contractive K `{Countable 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.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 50ceac0f10662f859749bf436c378496fb01ec93..d1f9f0c3bdd5e74929a5c32f90ca6add88e3f82a 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -186,7 +186,7 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
 Qed.
 
-(* CMRA *)
+(* CMRA. Only works if [A] has a unit! *)
 Section cmra.
   Context {A : ucmraT}.
   Implicit Types l : list A.
@@ -571,3 +571,6 @@ Instance listURF_contractive F :
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
+
+Definition listRF (F : urFunctor) : rFunctor :=
+  urFunctor_to_rFunctor $ listURF F.