proposition: Lemma beq_vec_ok1_cast : forall n (v : vector A n) p (w : vector A p) (leq : n = p), beq_vec v w = true -> Vcast v leq = w.
proof: Proof. induction v; destruct w; simpl; intros; try discr. rewrite Vcast_refl; refl. destruct (andb_elim H). rewrite beq_ok in H0. subst h0. rewrite Vcast_cons; simpl. f_equal; apply IHv. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)