proposition: Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : (∀ x, Proper ((≡) ==> impl) (P x)) → 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: Proof. intros ? Hemp Hadd. cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } induction 1 as [|x l ?? IH]; simpl. - intros X HX. setoid_rewrite elem_of_nil in HX. rewrite equiv_empty; [done|]. set_solver. - intros X HX. setoid_rewrite elem_of_cons in HX. rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd; [set_solver|]. apply IH; set_solver. Qed.
imports: stdpp(relations) stdpp(options)