proposition: Lemma rtc_split A (R : rel A) : R# << eq U R!.
proof: Proof. unfold incl, union. intros. elim H. intros. right. apply t_step. hyp. intro. left. refl. intros. destruct H1; destruct H3. left. trans y0; hyp. subst y0. right. hyp. subst y0. right. hyp. right. trans y0; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)