proposition: Lemma foldr_cons_permute {A} (R : relation A) `{!PreOrder R} (f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} x l : R (foldr f a (x :: l)) (foldr f (f x a) l).
proof: Proof. rewrite <-foldr_snoc. eapply foldr_permutation_proper'; [done..|]. rewrite Permutation_app_comm. done. Qed.
imports: stdpp(options)