proposition: Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) : vec_to_list v = vec_to_list w → v = w.
proof: Proof. revert w. induction v; intros w; inv_vec w; intros; simplify_eq/=; f_equal; eauto. Qed.
imports: stdpp(countable) stdpp(options)