proposition: Lemma Veq_sub_cons : forall n (v v' : vector A n) i (h : i<n), Vsub v (Veq_app_cons_aux1 h) = Vsub v' (Veq_app_cons_aux1 h) -> Vnth v h = Vnth v' h -> Vsub v (Veq_app_cons_aux2 h) = Vsub v' (Veq_app_cons_aux2 h) -> v = v'.
proof: Proof. intros. eapply Veq_sub_cons_aux; ehyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)