proposition: Theorem Proper_red : forall T U (rT : relation T) (rU : relation U) (f : T -> U), (forall x x', rT x x' -> rU (f x) (f x')) -> Proper (rT ==> rU) f.
proof: Proof. intuition. Qed.
imports: Setoid RelationClasses Morphisms