proposition: Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x : v !!! i = x ↔ (v : list A) !! (i : nat) = Some x.
proof: Proof. induction v as [|? ? v IH]; inv_fin i. - simpl; split; congruence. - done. Qed.
imports: stdpp(countable) stdpp(options)