proposition: Lemma Vsub_cast_aux : forall n (v : vector A n) n' (e : n=n') i k (h : i+k<=n') (h' : i+k<=n), Vsub (Vcast v e) h = Vsub v h'.
proof: Proof. destruct v; destruct n'; simpl; intros; try discr. rewrite Vcast_refl; apply Vsub_pi. inversion e; subst n'; rewrite Vcast_refl; apply Vsub_pi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)