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