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