proposition: Lemma Vcast_eq_intro : forall n (v1 v2 : vector A n) p (e : n=p), v1 = v2 -> Vcast v1 e = Vcast v2 e.
proof: Proof. induction v1; intros. subst v2. refl. rewrite H. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)