diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 5f26e17f1df82529f413e64320f4022d91a2b81c..95a475b6bf6f128c4553336496c8464003e11332 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -113,7 +113,7 @@ Qed.
 Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof.
   rewrite /inv (pvs_allocI N); first done.
-  (* FIXME use coPset_suffixes_infinite. *)
-Abort.
+  apply coPset_suffixes_infinite.
+Qed.
 
 End inv.