proposition: Lemma bsteps_nsteps n x y : bsteps R n x y ↔ ∃ n', n' ≤ n ∧ nsteps R n' x y.
proof: Proof. split. - induction 1 as [|n x1 x2 y ?? (n'&?&?)]. + exists 0; naive_solver eauto with lia. + exists (S n'); naive_solver eauto with lia. - intros (n'&Hn'&Hsteps). apply bsteps_weaken with n'; [done|]. clear Hn'. induction Hsteps; eauto. Qed.
imports: stdpp(options)