proposition: Lemma set_ind (P : C → Prop) : Proper ((≡) ==> impl) P → P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
proof: Proof. intros ? Hemp Hadd. apply well_founded_induction with (⊂). { apply set_wf. } intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX]. - rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd; [set_solver|]. apply IH; set_solver. - by rewrite HX. Qed.
imports: stdpp(relations) stdpp(options)