fact: Definition respectful {B} (R : crelation A) (R' : crelation B) : crelation (A -> B) := Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses