fact: Definition i_respectful {A B : Type -> Type} (RA : forall T, A T -> A T -> Prop) (RB : forall T, B T -> B T -> Prop) (f1 f2 : A ~> B) : Prop := forall T (a1 a2 : A T), RA T a1 a2 -> (RB T) (f1 T a1) (f2 T a2).
imports: Coq(Relations Setoid) ITree(Basics.Basics)