proposition: Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) : P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
proof: Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
imports: stdpp(relations) stdpp(options)