proposition: Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)} (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : Proper ((≡ₚ) ==> R) (foldr f b).
proof: Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
imports: stdpp(options)