proposition: Lemma sum_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; inv H. destruct H2 as (? & ? & ?); eexists; eauto. destruct H2 as (? & ? & ?); eexists; eauto. - destruct H as (? & H1 & H2); inv H1; inv H2. econstructor; eexists; eauto. econstructor; eexists; eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)