proposition: Lemma Veq_app_cons_aux : forall n (v : vector A n) i (h1 : 0 + i <= n) (h2 : i < n) (h3 : S i + (n - S i) <= n) (e : i + S (n - S i) = n), v = Vcast (Vapp (Vsub v h1) (Vcons (Vnth v h2) (Vsub v h3))) e.
proof: Proof. induction v; intros. apply Veq_nth; intros. lia. destruct i; simpl; rewrite Vcast_cons; f_equal; rewrite !Vsub_cons. apply Veq_nth; intros. rewrite Vnth_cast, Vnth_sub. apply Vnth_eq. lia. apply IHv. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)