proposition: Lemma transpose_inclusion : forall {A B} (R1 : relationH A B) (R2 : relationH A B), R1 ⊑ R2 <-> († R1 ⊑ † R2).
proof: Proof. intros A B R1 R2. split. - intros HS. unfold subrelationH, transpose in *. eauto. - intros HS. unfold subrelationH, transpose in *. eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)