proposition: Lemma beq_vec_ok_length : forall n (v : vector A n) p (w : vector A p), beq_vec v w = true -> n = p.
proof: Proof. induction v; destruct w; simpl; intros; try (refl || discr). destruct (andb_elim H). ded (IHv _ _ H1). subst n0. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)