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