diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index cab9674341fc025b1950ea702a423191c5e6e8b5..e71f698a407fa1f5823d7281592f7fe67a80d0eb 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -401,7 +401,7 @@ Section infinite.
 
   (** Properties about the [fresh] operation on finite sets *)
   Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
-  Proof. unfold fresh, set_fresh. solve_proper. Qed.
+  Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
 
   Lemma is_fresh X : fresh X ∉ X.
   Proof.