diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index e6a124cacfd8f9a08bbc326fcc7eb639fad039c2..13f796c51362d1e11e886ccabf8e4d725527137d 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -328,5 +328,13 @@ Proof.
   apply viewO_map_ne; by apply urFunctor_map_contractive.
 Qed.
 
-Definition authRF (F : urFunctor) :=
-  urFunctor_to_rFunctor (authURF F).
+Program Definition authRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
+|}.
+Solve Obligations with apply authURF.
+
+Instance authRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (authRF F).
+Proof. apply authURF_contractive. Qed.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 61fac88686b4f0f511cf08c7db9b5eabbd776c46..5b29880c0848286e32264edde9a1f6cfc417959b 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1575,8 +1575,15 @@ 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).
+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)
+|}.
+Solve Obligations with apply optionURF.
+
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof. apply optionURF_contractive. Qed.
 
 (* Dependently-typed functions over a discrete domain *)
 Section discrete_fun_cmra.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index b0832496ff8c9411557da2ff2b8474f2421e2fea..2f5974324acf63c88a1b48a558ea9794f4792aeb 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -718,5 +718,12 @@ 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).
+Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := gmapR K (rFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
+|}.
+Solve Obligations with apply gmapURF.
+
+Instance gmapRF_contractive K `{Countable K} F :
+  rFunctorContractive F → rFunctorContractive (gmapRF K F).
+Proof. apply gmapURF_contractive. Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 9aa39210779a5fd5cf85bfdbee53229fc3e344ad..e8b9af03465faf0ccdd24c08b7c3f829bc2192f4 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -572,5 +572,12 @@ 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).
+Program Definition listRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := listR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
+|}.
+Solve Obligations with apply listURF.
+
+Instance listRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (listRF F).
+Proof. apply listURF_contractive. Qed.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 0c49790826b31f5a487fd92bbb2f187c9b93594c..fb6601ad17a05177ceda026a7058bc4615af5f79 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -45,12 +45,12 @@ Ltac solve_inG :=
   repeat match goal with
          | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
          end;
-  (* Again get all assumptions *)
-  intros;
+  (* Again get all assumptions and simplify the functors *)
+  intros; simpl in *;
   (* We support two kinds of goals: Things convertible to inG;
      and records with inG and typeclass fields. Try to solve the
      first case. *)
-  try done;
+  try assumption;
   (* That didn't work, now we're in for the second case. *)
   split; (assumption || by apply _).
 
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 700ea958907efa23db79df679212c45d5cfdfcfd..87d3a7a7a9fc1a2ebb858b66bf2df8bf535e4c4b 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -19,8 +19,8 @@ Module invG.
 
   Definition invΣ : gFunctors :=
     #[GFunctor (gmap_viewRF positive (laterOF idOF));
-      GFunctor coPset_disjUR;
-      GFunctor (gset_disjUR positive)].
+      GFunctor coPset_disjR;
+      GFunctor (gset_disjR positive)].
 
   Class invPreG (Σ : gFunctors) : Set := WsatPreG {
     inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));