diff --git a/theories/vector.v b/theories/vector.v
index 3607efbe1473a54aa8e11bbba0652dfcbcd2629d..c81fa6603a96971c110fcc96b0062113a5df65d6 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -260,6 +260,10 @@ with value [x]. *)
 Fixpoint vreplicate {A} (n : nat) (x : A) : vec A n :=
   match n with 0 => [#] | S n => x ::: vreplicate n x end.
 
+Lemma vec_to_list_replicate {A} n (x : A) :
+  vec_to_list (vreplicate n x) = replicate n x.
+Proof. induction n; by f_equal/=. Qed.
+
 (* Vectors can be inhabited. *)
 Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
 Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=