proposition: Lemma rtc_split2 A (R : rel A) : R# << eq U R @ R#.
proof: Proof. unfold incl, union. intros. elim H; clear H x y; intros. right. exists y; split. exact H. refl. auto. destruct H0. subst y. destruct H2. auto. destruct H0. right. exists x0. auto. do 2 destruct H0. right. exists x0. split. exact H0. trans y; auto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)