proposition: Lemma tc_step_l 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 IHxy1; inversion IHxy2; right; solve [eauto | inversion H; try inversion H0; exists x0; [trivial | constructor 2 with y; auto]]. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)