proposition: Lemma transpose_sym_eq_rel {A} (R : relationH A A) {RS: Symmetric R} : † R ≡ R.
proof: Proof. unfold transpose; split; intros!; cbn in *. - apply SymmetricH_Symmetric in RS. unfold SymmetricH in RS. apply (RS y x). assumption. - apply SymmetricH_Symmetric in RS. unfold SymmetricH in RS. apply (RS x y). assumption. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)