proposition: Lemma rtc_union A (R S : rel A) : (R U S)# << (R# @ S)# @ R#.
proof: Proof. unfold incl. intros. elim H; intros. destruct H0. exists x0; split. refl. apply rt_step. exact H0. exists y0; split. apply rt_step. exists x0; split. refl. exact H0. refl. exists x0; split; refl. do 2 destruct H1. do 2 destruct H3. assert (h : ((R# @ S)# @ clos_refl_trans R) x1 x2). apply incl_elim with (R := (R# @ clos_refl_trans (R# @ S))). apply rtc_comp_permut. exists y0; split; hyp. destruct h. destruct H6. exists x3; split. trans x1; hyp. trans x2; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)