proposition: Lemma incl_rc_rtc A (R S : rel A) : R << S! -> R% << S#.
proof: Proof. intro. unfold incl. intros. destruct H0. subst y. refl. apply incl_elim with (R := S!). apply tc_incl_rtc. apply H. exact H0. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)