proposition: Lemma Vcast_sub : forall n (v : vector A n) i k (h : i + k <= n) j (e : k = j), Vcast (Vsub v h) e = Vsub v (Vcast_sub_aux1 h e).
proof: Proof. intros. apply Veq_nth. intros. rewrite Vnth_cast, !Vnth_sub. apply Vnth_eq. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)