Commit 5b46218d authored by Dan Frumin's avatar Dan Frumin

Add `awp_wand`

parent def619ad
......@@ -28,7 +28,20 @@ Section lifting.
rewrite /awp.
wp_pure _.
done.
Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
awp e R Φ -
( v, Φ v - Ψ v) -
awp e R Ψ.
Proof.
iIntros "HAWP Hv".
rewrite /awp.
iApply (wp_wand with "HAWP").
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hunfl".
iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ".
iIntros (w) "[HΦ $]". by iApply "Hv".
Qed.
End lifting.
......
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