proposition: Lemma SymmetricH_Symmetric {A: Type} (R : relationH A A) : SymmetricH R <-> Symmetric R.
proof: Proof. split; intros. - red. unfold SymmetricH in H. intros. specialize (H x y). cbn in H. apply H. assumption. - red. intros p HP. cbn in *. apply H. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)