proposition: Lemma nsteps_list n x y : nsteps 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. setoid_rewrite head_lookup. split. - induction 1 as [x|n' x x' y ?? IH]. { exists [x]; naive_solver. } destruct IH as (l & Hlen & Hfirst & Hlast & Hcons). exists (x :: l). simpl. rewrite Hlen, last_cons, Hlast. split_and!; [done..|]. intros [|i]; naive_solver. - intros ([|x' l]&?&Hfirst&Hlast&Hcons); simplify_eq/=. revert x Hlast Hcons. induction l as [|x1 l IH]; intros x2 Hlast Hcons; simplify_eq/=; [constructor|]. econstructor; [by apply (Hcons 0)|]. apply IH; [done|]. intros i. apply (Hcons (S i)). Qed.
imports: stdpp(options)