diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 576bf4fad16690cc10d235b1d88ab765cbb7fa4c..c85e5833286cea3b3d85453aec255a915bcb6a79 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -157,6 +157,9 @@ Proof.
     apply Hadd. set_solver. apply IH; set_solver.
   - by rewrite HX.
 Qed.
+Lemma collection_ind_L `{!LeibnizEquiv C} (P : C → Prop) :
+  P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
+Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
 
 (** * The [collection_fold] operation *)
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :