proposition: Lemma rtc_list x y : rtc R x y ↔ ∃ 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 rtc_bsteps. split. - intros (n'&(l&?&?&?&?)%bsteps_list). exists l; eauto with lia. - intros (l&?&?&?). exists (pred (length l)). apply bsteps_list. exists l. eauto with lia. Qed.
imports: stdpp(options)