proposition: Lemma PER_reflexivityH2 : forall {A:Type} (R : relationH A A) (RS: SymmetricH R) (RT: TransitiveH R) (a b : A), R b a -> R a a.
proof: Proof. intros. assert (R a b). { specialize (RS b a). apply RS. assumption. } specialize (RT a b a). apply RT; auto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)