From 84fd0660f9dbd3cb4c007c0fcc8d2e00a1af077f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 May 2019 10:25:31 +0200
Subject: [PATCH] Add `set_fold_ind_L`.

---
 theories/fin_sets.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 743d6f3e..cab96743 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))) :
-- 
GitLab