proposition: Lemma beq_vec_ok : forall n (v w : vector A n), beq_vec v w = true <-> v = w.
proof: Proof. split; intro. apply beq_vec_ok1. hyp. apply beq_vec_ok2. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)