diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 743d6f3ebc29a7b201bb83581a4adca0748be69a..cab9674341fc025b1950ea702a423191c5e6e8b5 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -224,6 +224,11 @@ Proof.
     rewrite (union_difference {[ x ]} X) by set_solver.
     apply Hadd. set_solver. apply IH. set_solver.
 Qed.
+Lemma set_fold_ind_L `{!LeibnizEquiv C}
+    {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+  ∀ X, P (set_fold f b X) X.
+Proof. apply set_fold_ind. by intros ?? -> ?? ->%leibniz_equiv. Qed.
 Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :