proposition: Lemma foldr_comm_acc_strong {A B} (R : relation B) `{!PreOrder R} (f : A → B → B) (g : B → B) b l : (∀ x, Proper (R ==> R) (f x)) → (∀ x y, x ∈ l → R (f x (g y)) (g (f x y))) → R (foldr f (g b) l) (g (foldr f b l)).
proof: Proof. intros ? Hcomm. induction l as [|x l IH]; simpl; [done|]. rewrite <-Hcomm by eauto using elem_of_list_here. by rewrite IH by eauto using elem_of_list_further. Qed.
imports: stdpp(options)