Commit 48d958f2 authored by Robbert Krebbers's avatar Robbert Krebbers

Induction principle for finite sets with Leibniz equality.

parent e4090611
......@@ -157,6 +157,9 @@ Proof.
apply Hadd. set_solver. apply IH; set_solver.
- by rewrite HX.
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) :
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment