proposition: Lemma tc_merge A (R : rel A) : R @ R# << R!.
proof: Proof. unfold incl. intros. destruct H. destruct H. ded (rtc_split H0). destruct H1; subst. apply t_step; hyp. trans x0. apply t_step. hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)