diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index f0af0c92d7bdada3ee3ffc54ad78e36d6f36266c..ecccd40bd19b4573a1169d0357d15840d3120623 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -145,7 +145,7 @@ Proof.
 Qed.
 
 Lemma collection_wf : wf (strict (@subseteq C _)).
-Proof. apply well_founded_lt_compat with size, subset_size. Qed.
+Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
 
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →