proposition: Lemma prod_compose {A B C D E F: Type} (R: relationH A B) (S: relationH B C) (T: relationH D E) (U: relationH E F) : (S ∘ R) ⊗ (U ∘ T) ≡ (S ⊗ U) ∘ (R ⊗ T).
proof: Proof. split; intros!. - destruct x, y. repeat red. repeat red in H. destruct H as [H1 H2]. unfold fst, snd. cbn in H1, H2. edestruct H1 as (b & HR & HS). edestruct H2 as (e & HT & HU). exists (b, e). split; cbn; split; eauto. - destruct x, y. repeat red. repeat red in H. destruct H as [x [H1 H2]]. split. + exists (fst x). cbn; split; [apply H1|apply H2]. + exists (snd x). cbn; split; [apply H1|apply H2]. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)