proposition: Lemma comp_clos_eq R : same (comp_clos R) (E @ (R @ E)).
proof: Proof. split. intros t u tu. inversion_clear tu; subst. ex u'. intuition. ex v'. intuition. intros t u [t' [tt' [u' [t'u' u'u]]]]. eapply comp_clos_intro. apply tt'. sym. apply u'u. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)