proposition: Lemma tc_split_inv A (R : rel A) : R# @ R << R!.
proof: Proof. intros x y RRxy. destruct RRxy as [z [Rxz Rzy]]. destruct (rtc_split Rxz). rewrite H. intuition. constructor 2 with z. hyp. constructor 1. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)