Avoid relying on `Export` bugs

See https://github.com/coq/coq/issues/10480 and https://github.com/coq/coq/issues/10474.

This should be compatible with Coq's master, but I haven't tested.

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. Morphisms.solve_proper. Qed.
 
   Lemma is_fresh X : fresh X ∉ X.
   Proof.