proposition: Lemma Vforall_cast : forall n v p (h : n=p), Vforall (Vcast v h) <-> Vforall v.
proof: Proof. intros n v p h. rewrite 2!Vforall_eq. intuition. apply H. rewrite Vin_cast. hyp. apply H. rewrite Vin_cast in H0. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)