proposition: Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') : subrelation (RA ==> RB) (RA' ==> RB').
proof: Proof. simpl_crelation. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses