Solution for WPsem.WpFromTriple2.wp_equiv_2
unfold wp_2. iff M.
{ applys triple_named_heap. intros h K.
applys triple_conseq (fun h' => h' = h) Q.
{ specializes M K. applys M. }
{ intros ? ->. auto. }
{ applys qimpl_refl. } }
{ intros h K. unfold wp_2. applys triple_conseq M.
{ intros h' ->. applys K. }
{ applys qimpl_refl. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
