proposition: Lemma set_fold_ind_L `{!LeibnizEquiv C} {B} (P : B → C → Prop) (f : A → B → B) (b : B) : 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. apply set_fold_ind. solve_proper. Qed.
imports: stdpp(relations) stdpp(options)