proposition: Lemma tc_union A (R S : rel A) : (R U S)! << R! U (R# @ S)! @ R#.
proof: Proof. unfold incl. induction 1. destruct H. left. apply t_step. exact H. right. exists y. intuition. apply t_step. exists x. intuition. destruct IHclos_trans1. destruct IHclos_trans2. left. trans y; hyp. right. do 2 destruct H2. exists x0. intuition. apply rtc_comp_modulo. exists y. intuition. apply tc_incl_rtc. exact H1. right. do 2 destruct H1. destruct IHclos_trans2. exists x0. intuition. trans y. exact H2. apply tc_incl_rtc. exact H3. do 2 destruct H3. exists x1. intuition. trans x0. exact H1. apply rtc_comp_modulo. exists y. intuition. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)