proposition: Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) : vec_to_list v = vec_to_list w → n = m.
proof: Proof. revert m w. induction v; intros ? [|???] ?; simplify_eq/=; f_equal; eauto. Qed.
imports: stdpp(countable) stdpp(options)