proposition: Lemma Veq_app : forall n (v : vector A n) i (h : i<=n), v = Vcast (Vapp (Vsub v (Veq_app_aux1 h)) (Vsub v (Veq_app_aux2 h))) (Veq_app_aux3 h).
proof: Proof. intros. apply Veq_app_aux. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)