proposition: Lemma eqb_eq: forall n (v1: t A n) (v2: t A n), eqb v1 v2 = true <-> v1 = v2.
proof: Proof. refine (@rect2 _ _ _ _ _); [now constructor | simpl]. intros ? ? ? Hrec h1 h2; destruct Hrec; destruct (A_eqb_eq h1 h2); split. + intros Hbeq. apply andb_prop in Hbeq; destruct Hbeq. f_equal; now auto. + intros Heq. destruct (cons_inj Heq). apply andb_true_intro. split; now auto. Qed.
imports: VectorDef VectorSpec