Commit 12968f8d authored by Dan Frumin's avatar Dan Frumin

ElimModal |==> instance for awp

parent 2cc2993e
......@@ -70,6 +70,18 @@ Section a_wp.
unflocked γ π -
WP ev env l {{ v, Φ v unflocked γ π }}
}})%I.
Global Instance elim_bupd_awp p e Φ :
ElimModal True p false (|==> P) P
(awp e R Φ) (awp e R Φ).
Proof.
iIntros (P R _) "[HP HA]".
rewrite /awp /tc_opaque.
destruct p; simpl;
[ iDestruct "HP" as "#HP" | ];
iMod "HP"; by iApply "HA".
Qed.
End a_wp.
Section a_wp_rules.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment