proposition: Lemma Vreplace_pi : forall n (v : vector A n) i1 i2 (h1 : i1 < n) (h2 : i2 < n) x, i1 = i2 -> Vreplace v h1 x = Vreplace v h2 x.
proof: Proof. intros. subst i2. revert i1 h1 h2. elim v; clear v; simpl; intros. lia. destruct i1. refl. apply Vtail_eq. apply H. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)