diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 0aaf5bd51f62eaba268257d52e9cce1ba1de841f..8b49383585e4406462844dbed4cdaff09727eb74 100644
--- a/prelude/fin_collections.v
+++ b/prelude/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) :