Commit 0c5631c4 authored by Ralf Jung's avatar Ralf Jung

use WP sugar

parent f530c3ec
......@@ -242,7 +242,7 @@ Lemma wp_wand_r s E e Φ Ψ :
WP e @ s; E {{ Φ }} ( v, Φ v - Ψ v) WP e @ s; E {{ Ψ }}.
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Lemma wp_frame_wand_l s E e Q Φ :
Q WP e @ s; E {{ λ v, Q - Φ v }} - WP e @ s; E {{ Φ }}.
Q WP e @ s; E {{ v, Q - Φ v }} - WP e @ s; E {{ Φ }}.
Proof.
iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
iIntros (v) "HΦ". by iApply "HΦ".
......
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