proposition: Lemma to_list_rev_append_tail A n m (v1 : t A n) (v2 : t A m): to_list (rev_append_tail v1 v2) = List.rev_append (to_list v1) (to_list v2).
proof: Proof. now revert m v2; induction v1 as [ | ? ? ? IHv1 ]; intros; [ | simpl; rewrite IHv1 ]. Qed.
imports: VectorDef PeanoNat Eqdep_dec