proposition: Lemma beq_vec_refl : forall n (v : vector A n), beq_vec v v = true.
proof: Proof. induction v; simpl. refl. apply andb_intro. apply (beq_refl beq_ok). exact IHv. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)