From 48d958f2ff9fd51d40b8cc1386da57fe2078d2e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Sep 2016 10:05:48 +0200
Subject: [PATCH] Induction principle for finite sets with Leibniz equality.

---
 prelude/fin_collections.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 0aaf5bd51..8b4938358 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) :
-- 
GitLab