proposition: Lemma rtc_comp_permut A (R S : rel A) : R# @ (R# @ S)# << (R# @ S)# @ R#.
proof: Proof. unfold incl. intros. do 2 destruct H. ded (rtc_split2 H0). destruct H1. subst x0. exists x; split. refl. exact H. do 4 destruct H1. exists y; split. trans x1. apply rt_step. exists x2; split. trans x0; hyp. hyp. hyp. refl. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)