fact: Record prod_rel {A1 A2 B1 B2 : Type} (RA : relationH A1 A2) (RB : relationH B1 B2) (p1 : A1 * B1) (p2 : A2 * B2) : Prop := prod_morphism { fst_rel : RA (fst p1) (fst p2) ; snd_rel : RB (snd p1) (snd p2) }.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)