proposition: Lemma transpose_monotone {A B} (R S: relationH A B) `{R ⊑ S} : †R ⊑ †S.
proof: Proof. unfold transpose; intros!. apply H. auto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)