proposition: Lemma sum_rel_monotone {A B C D: Type} (R R': relationH A B) (S S': relationH C D) `{R ⊑ R'} `{S ⊑ S'} : R ⊕ S ⊑ R' ⊕ S'.
proof: Proof. intros!; destruct x, y; repeat red; repeat red in H1; inversion H1; subst; constructor; eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)