proposition: Lemma pointwise_Proper {A B} R (f : A -> B) `{forall x, Proper R (f x)} : Proper (pointwise_relation A R) f.
proof: Proof. unfold Proper in *. repeat intro; trivial. Qed.
imports: Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat