proposition: Theorem eqb_vector_refl : forall (A : Set)(eqd : EqDec A)(n : nat)(v : Vector.t A n), eqb_vector _ v v = true.
proof: Proof. induction n; intuition; simpl in *. rewrite (vector_0 v). unfold eqb_vector. simpl. trivial. destruct (vector_S v). destruct H. subst. unfold eqb_vector. simpl. rewrite eqb_refl. eapply IHn. Qed.
imports: Bvector Arith