proposition: Lemma transpose_involution : forall {A B} (R : relationH A B), † † R ≡ R.
proof: Proof. intros A B R. split. - unfold subrelationH. unfold transpose. tauto. - unfold subrelationH, transpose. tauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)