Skip to content

add wp_frame_wand lemma

Ralf Jung requested to merge ralf/wp_frame_wand into master

This lemma makes it very easy to add Q -∗ to the postcondition:

iApply (wp_frame_wand with "HQ").
Edited by Ralf Jung

Merge request reports