proposition: Lemma tc_incl_trans A (R S : rel A) : Transitive S -> R << S -> R! << S.
proof: Proof. intros S_trans RS. intros t u tu; revert t u tu. induction 1; fo. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)