diff --git a/theories/vector.v b/theories/vector.v
index 17f1b8f10bfa07f731409dec7aa6c6886b1c24b2..db1f678ef53257a0cdf2cdb8a3ab8aa293d6f694 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -41,9 +41,6 @@ Proof.
   refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
 Defined.
 
-(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
-type class, as it has a dependent type. *)
-Arguments Vector.nth {_ _} !_ !_%fin /.
 Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
   fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
   match i in fin m return vec A m → A with