proposition: Lemma to_list_append A n m (v1 : t A n) (v2 : t A m): to_list (append v1 v2) = List.app (to_list v1) (to_list v2).
proof: Proof. induction v1; simpl; trivial. now rewrite to_list_cons; f_equal. Qed.
imports: VectorDef PeanoNat Eqdep_dec