proposition: Lemma vlookup_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i : vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
proof: Proof. vec_double_ind v1 v2. - intros i; inv_fin i. - intros n v1 v2 IH a b i. inv_fin i; eauto. Qed.
imports: stdpp(countable) stdpp(options)