proposition: Lemma Vnth_app_cons_neq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) k (h : k < n1 + S n2) x x', k <> n1 -> Vnth (Vapp v1 (Vcons x v2)) h = Vnth (Vapp v1 (Vcons x' v2)) h.
proof: Proof. induction v1; intros. simpl. destruct k. cong. refl. rewrite !Vapp_cons. destruct k. refl. apply IHv1. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)