proposition: Lemma vec_to_list_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) : vec_to_list (vzip_with f v1 v2) = zip_with f (vec_to_list v1) (vec_to_list v2).
proof: Proof. revert v2. induction v1 as [|??? IHv1]; intros v2; inv_vec v2; intros; simpl; [done|]. by rewrite IHv1. Qed.
imports: stdpp(countable) stdpp(options)