proposition: Lemma transpose_sum {A B C D: Type} (R: relationH A B) (S: relationH C D) : † (S ⊕ R) ≡ (†S ⊕ †R).
proof: Proof. split; unfold transpose; cbn; intros!; destruct x, y; cbn in *; try inversion H; eauto; subst; inversion H; subst; try econstructor; eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)