proposition: Lemma tc_absorbs_left A (R S : rel A) : R @ S << S -> R @ S! << S!.
proof: Proof. intro. unfold incl. intros. do 2 destruct H0. generalize x0 y H1 H0. induction 1; intros. apply t_step. apply H. exists x1; split; hyp. trans y0; auto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)