proposition: Lemma sum_rel_eq : forall (A B: Type), @eq A ⊕ @eq B ≡ @eq (A + B).
proof: Proof. intros. red. split; repeat intro; eauto. inversion H; subst; auto; try reflexivity. subst. destruct y; constructor; eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)