proposition: Lemma Veq_sub_cons_aux : forall n (v v' : vector A n) i (h1 : 0+i<=n) (h2 : i<n) (h3 : S i+(n-S i)<=n), Vsub v h1 = Vsub v' h1 -> Vnth v h2 = Vnth v' h2 -> Vsub v h3 = Vsub v' h3 -> v = v'.
proof: Proof. intros. assert (e:i+S(n-S i)=n). lia. rewrite (Veq_app_cons_aux v h1 h2 h3 e), (Veq_app_cons_aux v' h1 h2 h3 e). apply Vcast_eq_intro. apply Vapp_eq_intro. hyp. apply Vcons_eq_intro; hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)