proposition: Lemma beq_vec_ok2 : forall n (v w : vector A n), v = w -> beq_vec v w = true.
proof: Proof. induction v; intros. VOtac. refl. VSntac w. rewrite H0 in H. Veqtac. subst h. subst v. simpl. rewrite (beq_refl beq_ok). simpl. apply beq_vec_refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)