proposition: Lemma bsteps_list n x y : bsteps R n x y ↔ ∃ l, length l ≤ S n ∧ 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 bsteps_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. split; [|by eauto]. by destruct l. Qed.
imports: stdpp(options)