proposition: Lemma foldr_comm_acc {A} (f : A → A → A) (g : A → A) (a : A) l : (∀ x y, f x (g y) = g (f x y)) → foldr f (g a) l = g (foldr f a l).
proof: Proof. intros. apply (foldr_comm_acc_strong _); [solve_proper|done]. Qed.
imports: stdpp(options)