prove pvs_alloc

395e0918 · Ralf Jung · 6d2ac942 · 395e0918
Commit 395e0918 authored Feb 09, 2016 by Ralf Jung
--- 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.