proposition: Lemma to_list_inj A n (v w : t A n): to_list v = to_list w -> v = w.
proof: Proof. revert v. induction w as [| w0 n w IHw]. - apply to_list_nil_iff. - intros v H. rewrite (eta v) in H. injection H as [=H0 H1%IHw]. subst. apply eta. Qed.
imports: VectorDef PeanoNat Eqdep_dec