Commit 7ee261cf authored by Ralf Jung's avatar Ralf Jung
Browse files

use wp_frame_wand where suitable

parent 09835135
......@@ -112,7 +112,7 @@ Section lemmas.
Φ, .. x, α x - (.. y, β x y - Φ (f x y)) - WP e {{ Φ }}.
rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
Supports Markdown
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