Solution for WPsem.WpFromTriple.wp_equiv_1
unfold wp_1. iff M.
{ applys triple_conseq Q M.
{ applys triple_hexists. intros H'.
rewrite hstar_comm. applys triple_hpure.
intros N. applys N. }
{ xsimpl. } }
{ xsimpl. apply M. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
