proposition: Lemma incl_rt1_union_union A (R S : rel A) : (R!1 U S!1)#1 << (R U S)#1.
proof: Proof. intros x y xRy. induction xRy. refl. apply rtc1_preorder with y; trivial. destruct H. apply union_rel_rt1_left. apply tc1_incl_rtc1. hyp. apply union_rel_rt1_right. apply tc1_incl_rtc1. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)