Solution for WPsem.wp_equiv_iff_wp_pre_and_wp_weakest
iff (M1&M2) M.
{ introv. iff M.
{ applys triple_conseq M1 M. auto. }
{ applys M2. auto. } }
{ split.
{ intros. rewrite <- M. applys himpl_refl. }
{ introv R. rewrite M. applys R. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
