proposition: Lemma prod_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. destruct H1. split. - apply H. assumption. - apply H0. assumption. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)