proposition: Lemma tc_step_r A (R : rel A) x y : R! x y -> R x y \/ (exists2 z, R! x z & R z y).
proof: Proof. compute; intro xy; induction xy. left; trivial. inversion_clear IHxy1; inversion_clear IHxy2; right; solve [eauto | inversion H0; exists x0; [constructor 2 with y; auto | trivial]]. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)