Solution for WPsem.wp_if'
dup.
{ (* Proof from [wp_if] *)
intros. applys himpl_trans wp_if. case_if~. }
{ (* Proof from [triple_if] *)
intros. intros h K. applys* eval_if. case_if*. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
