proposition: Lemma ReflexiveH_Reflexive {A: Type} (R : relationH A A) : ReflexiveH R <-> Reflexive R.
proof: Proof. split; intros. - red. apply H. - apply H. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)