Solution for WPsem.wp_conseq_frame
dup 4.
{ (* Proof using [wp_ramified_trans] *)
introv M. applys wp_ramified_trans Q1. xsimpl. xchange M. }
{ (* Proof using [wp_conseq_frame_trans]. *)
introv M. applys* wp_conseq_frame_trans M. }
{ (* Proof using [wp_frame] and [wp_conseq_trans]. *)
introv M. applys* wp_conseq_trans M. applys* wp_frame. }
{ (* Proof using [triple_conseq_frame]. *)
introv M. rewrite wp_equiv.
applys triple_conseq_frame (wp t Q1) M.
{ rewrite <- wp_equiv. xsimpl. } { xsimpl. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
