proposition: Lemma Vnth_replace : forall n i (ip ip' : i < n) (v : vector A n) (a : A), Vnth (Vreplace v ip a) ip' = a.
proof: Proof. induction n; intros. lia. VSntac v. destruct i. trivial. simpl. apply IHn. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)