proposition: Lemma equiv_eq {A : Type} : forall n (v w : t A n), v == w -> v = w.
proof: Proof. intros n v w. pattern n, v, w; apply vector_double_rect. - reflexivity. - intros n0 v1 v2 a b H H0; red in H0. repeat rewrite to_list_cons in H0. injection H0. intros; subst b. f_equal; auto. Qed.
imports: Bool Arith Vector