diff --git a/theories/logic/satisfiable.v b/theories/logic/satisfiable.v
index 7ea61a8f6b9da6330debc6c6902e0a191c48de9e..4ca6546c4a13bddb3030d6b232d7f8b67b9ea05e 100644
--- a/theories/logic/satisfiable.v
+++ b/theories/logic/satisfiable.v
@@ -30,7 +30,7 @@ Section satisfiable.
 
     Global Instance sat_equiv: Proper ((≡) ==> iff) sat.
     Proof.
-      intros P Q Heq; split; intros Hsat; eauto using sat_mono, equiv_entails_1_1, equiv_entails_1_2.
+      intros P Q Heq; split; intros Hsat; (eapply sat_mono; last done); eauto using equiv_entails_1_1, equiv_entails_1_2.
     Qed.
 
     Lemma sat_sep P Q: sat (P ∗ Q) → sat P ∧ sat Q.