proposition: Lemma trans_rtc_incl A (R : rel A) : Reflexive R -> Transitive R -> R# << R.
proof: Proof. intros R_refl R_trans x y. induction 1. hyp. refl. trans y; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)