proposition: Lemma tc_split A (R : rel A) : R! << R @ R#.
proof: Proof. unfold incl. induction 1. exists y. split. hyp. refl. destruct IHclos_trans1. destruct H1. exists x0. split. hyp. trans y. hyp. apply incl_elim with (R:=R!). apply tc_incl_rtc. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)