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