Remove possibly costly call to auto in From/IntoTExist.

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) =>