fact: Definition rel_compose {A B C} (S : relationH B C) (R : relationH A B): relationH A C := fun x y => exists b, R x b /\ S b y.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)