proposition: Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n) (Hbeq: eqb v1 v2 = true), m = n.
proof: Proof. intros m n v1; revert n. induction v1; intros ? v2; destruct v2; [now constructor | discriminate | discriminate | simpl]. intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq. f_equal; eauto. Qed.
imports: VectorDef VectorSpec