diff --git a/theories/util_instances.v b/theories/util_instances.v
index a75c284cc70ae410628ca2152d36b6d6ebee80e6..f7cbbb0a6d6770835db902436b2c37bef1d795ae 100644
--- a/theories/util_instances.v
+++ b/theories/util_instances.v
@@ -724,12 +724,15 @@ Global Hint Extern 0 (FromExistCareful ?L ?R) =>
     end in 
   solve : typeclass_instances.
 
+Lemma exactly_entails {PROP : bi} (P : PROP) : P ⊢ P.
+Proof. done. Qed.
+
 Global Hint Extern 4 (FromTExistDirect (bi_exist ?input_fun) ?TT ?Q') =>
   match get_biexist_function_and_tele input_fun with
   | (?output_fun, ?telescope) =>
     unify TT telescope;
     unify output_fun Q';
-    by rewrite /FromTExistDirect /FromTExist
+    refine (exactly_entails _)
   end : typeclass_instances.
 
 Global Hint Extern 4 (IntoTExistExact (bi_exist ?input_fun) ?TT ?Q') =>
@@ -737,7 +740,7 @@ Global Hint Extern 4 (IntoTExistExact (bi_exist ?input_fun) ?TT ?Q') =>
   | (?output_fun, ?telescope) =>
     unify TT telescope;
     unify output_fun Q';
-    by rewrite /IntoTExistExact /IntoTExist
+    refine (exactly_entails _)
   end : typeclass_instances.
 
 Global Hint Extern 4 (FindInContext ?Δ ?PTC ?k ?r ?R) =>