proposition: Lemma TransitiveH_Transitive {A: Type} (R : relationH A A) : TransitiveH R <-> Transitive R.
proof: Proof. split; intros. - red. intros x y z H0 H1. unfold TransitiveH in H. eapply H; eauto. - red. intros p q HP HQ EQ. unfold Transitive in H. cbn in EQ. eapply H; eauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)