proposition: Lemma Vmap_first_cast : forall n (v : vector A n) n' (h : n=n'), Vmap_first (Vcast v h) = Vmap_first v.
proof: Proof. destruct v; intros; destruct n'; try discr. rewrite Vcast_refl. refl. inversion h0. subst n'. rewrite Vcast_refl. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)