proposition: Lemma Veq_app_cons : forall n (v : vector A n) i (h : i<n), v = Vcast (Vapp (Vsub v (Veq_app_cons_aux1 h)) (Vcons (Vnth v h) (Vsub v (Veq_app_cons_aux2 h)))) (Veq_app_cons_aux3 h).
proof: Proof. intros. apply Veq_app_cons_aux. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)