fact: Definition respectful_eq_itree {E F : Type -> Type} : (itree E ~> itree F) -> (itree E ~> itree F) -> Prop := i_respectful (fun _ => eq_itree eq) (fun _ => eq_itree eq).
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Core.Subevent Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp)