proposition: Lemma list_to_vec_to_list {A n} (v : vec A n) : list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (vec_to_list_length v)).
proof: Proof. apply vec_to_list_inj2. rewrite vec_to_list_to_vec. by destruct (eq_sym (vec_to_list_length v)). Qed.
imports: stdpp(countable) stdpp(options)