proposition: Lemma to_list_rev A n (v : t A n): to_list (rev v) = List.rev (to_list v).
proof: Proof. unfold rev; rewrite (plus_n_O n); unfold eq_rect_r; simpl. now rewrite to_list_rev_append, List.rev_alt. Qed.
imports: VectorDef PeanoNat Eqdep_dec