proposition: Lemma Vsub_cast : 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 (Vsub_cast_aux1 e h).
proof: Proof. intros. apply Vsub_cast_aux. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)