Solution for WPsem.wp_conseq_of_wp_ramified
dup.
{ introv M. applys wp_ramified_trans Q1. xsimpl. applys M. }
{ introv M. applys himpl_trans (wp t Q1 \* (Q1 \--* Q2)).
{ xsimpl. applys M. }
{ applys wp_ramified. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
