proposition: Theorem eqb_vector_leibniz: forall (A : Set)(eqd : EqDec A)(n : nat)(v1 v2 : Vector.t A n), eqb_vector _ v1 v2 = true -> v1 = v2.
proof: Proof. induction n; intuition; simpl in *. rewrite (vector_0 v1). rewrite (vector_0 v2). trivial. destruct (vector_S v1). destruct (vector_S v2). destruct H0. destruct H1. subst. unfold eqb_vector in H. simpl in *. case_eq (eqb x x0); intuition. rewrite eqb_leibniz in H0. subst. f_equal. rewrite eqb_refl in H. eapply IHn. eapply H. rewrite H0 in H. rewrite vector_fold_false in H. discriminate. Qed.
imports: Bvector Arith