proposition: Lemma beq_vec_ok1 n (v w : vector A n) : beq_vec v w = true -> v = w.
proof: Proof. intro. rewrite <- (Vcast_refl v (eq_refl n)). apply beq_vec_ok1_cast. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)