state_update_pgl_Wp

logsem · Feb 3, 2025 · af8aa97 · af8aa97
1 parent a5c0ee2
commit af8aa97
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
@@ -567,6 +567,12 @@ Section state_update.
     iMod ("H" with "[$]").
     by iModIntro.
   Qed.
+
+  Lemma state_update_pgl_wp  Φ E e:
+    state_update E E (WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
+  Proof.
+    iIntros ">$".
+  Qed.
 
   (** state_update works for allocation of invariants and ghost resources *)
   Lemma state_update_inv_alloc E P N: