proposition: Lemma Vnth_app_cons : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) (h : n1 < n1 + S n2) x, Vnth (Vapp v1 (Vcons x v2)) h = x.
proof: Proof. induction v1; intros; simpl. refl. apply IHv1. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)