proposition: Lemma Vreplace_nth_eq : forall n (v : vector A n) i (h : i < n), Vreplace v h (Vnth v h) = v.
proof: Proof. intros. apply Veq_nth. intro j. case (eq_nat_dec i j); intro Eij. rewrite <- Eij. intro hj. rewrite (Vnth_eq v h hj); auto. apply Vnth_replace. intro hj. apply Vnth_replace_neq; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)