proposition: Lemma tc_list x y : tc R x y ↔ ∃ l, 1 < length l ∧ head l = Some x ∧ last l = Some y ∧ ∀ i a b, l !! i = Some a → l !! S i = Some b → R a b.
proof: Proof. rewrite tc_nsteps. split. - intros (n'&?&(l&?&?&?&?)%nsteps_list). exists l; eauto with lia. - intros (l&?&?&?&?). exists (pred (length l)). split; [lia|]. apply nsteps_list. exists l. eauto with lia. Qed.
imports: stdpp(options)