proposition: Lemma Vmap_cast : forall m n (H : m=n) (v : vector A m), Vmap (Vcast v H) = Vcast (Vmap v) H.
proof: Proof. intros until H. case H. intro v. rewrite !Vcast_refl. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)