diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b5176725dfeb0dcb969e69dd0e15d3f286140d1a..a2926d819a884fc3b5b946c47ec7bd3bbf0ef3f6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -248,8 +248,9 @@ Global Instance from_later_exist {A} n (Φ Ψ : A → uPred M) :
 Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
 
 (* IntoWand *)
-Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
-Proof. done. Qed.
+Global Instance wand_weaken_assumption P1 P2 Q :
+  FromAssumption false P2 P1 → WandWeaken P1 Q P2 Q | 0.
+Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
 Global Instance wand_weaken_later P Q P' Q' :
   WandWeaken P Q P' Q' → WandWeaken' P Q (▷ P') (▷ Q').
 Proof.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index e44f27ce351ae74eaadb94f1b024e23a1c24110a..3b82f5140039cd87a9979688fb58b8b56ee2c249 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -78,8 +78,6 @@ Class WandWeaken' {M} (P Q P' Q' : uPred M) :=
   wand_weaken' :> WandWeaken P Q P' Q'.
 Hint Mode WandWeaken' + - - ! - : typeclass_instances.
 Hint Mode WandWeaken' + - - - ! : typeclass_instances.
-Instance wand_weaken_exact {M} (P Q : uPred M) : WandWeaken P Q P Q | 1000.
-Proof. done. Qed.
 
 Class IntoWand {M} (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
 Arguments into_wand {_} _ _ _ {_}.