proposition: Lemma rtc_comp_modulo A (R S : rel A) : R# @ (R# @ S)! << (R# @ S)!.
proof: Proof. unfold incl. intros. do 2 destruct H. ded (tc_split H0). do 2 destruct H1. do 2 destruct H1. ded (rtc_split H2). destruct H4. subst x1. apply t_step. exists x2. intuition. trans x0; hyp. trans x1. apply t_step. exists x2. intuition. trans x0; hyp. exact H4. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)