proposition: Lemma rtc1_union A (R S : rel A) : (R U S)#1 << (S#1 @ R)#1 @ S#1.
proof: Proof. intros x y xRSy. induction xRSy as [ | x y z xRSy yRSz]. exists x. split; refl. destruct IHyRSz as [m [ym mz]]. destruct ym as [m | m n o mn no]. induction xRSy as [xRy | xSy]. exists m. split; trivial. apply rt1_trans with m. exists x. split; trivial. refl. refl. exists x. split. refl. apply rt1_trans with m; trivial. exists o. split; trivial. induction xRSy as [xRy | xSy]. apply rt1_trans with m. exists x. split. refl. hyp. apply rtc1_preorder with n; trivial. apply rt1_trans with n; trivial. refl. apply rt1_trans with n. destruct mn as [q [mq qn]]. exists q. split; trivial. apply rt1_trans with m; hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)