proposition: Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x : ∃ i : fin (n + S m), x = (v +++ x ::: w) !!! i.
proof: Proof. induction v as [|??? IHv]; simpl; [by eexists 0%fin|]. destruct IHv as [i ?]. by exists (FS i). Qed.
imports: stdpp(countable) stdpp(options)