proposition: Lemma to_list_rev_append A n m (v1 : t A n) (v2 : t A m): to_list (rev_append v1 v2) = List.rev_append (to_list v1) (to_list v2).
proof: Proof. unfold rev_append; rewrite <- (Nat.tail_add_spec n m); apply to_list_rev_append_tail. Qed.
imports: VectorDef PeanoNat Eqdep_dec