proposition: Lemma Vreplace_eq_elim : forall n (v : vector A n) i (h : i < n) x x', Vreplace v h x = Vreplace v h x' -> x = x'.
proof: Proof. intros. ded (f_equal (fun v => @Vnth A n v i h) H). rewrite !Vnth_replace in H0. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)