Solution for Himpl.XsimplTactic.EntailmentProofs.himpl_example_2
intros. rewrite hstar_comm. rewrite hstar_assoc.
applys himpl_hstar_hpure_l. intros H1.
rewrites hstar_assoc. rewrite hstar_comm. rewrite hstar_assoc.
applys himpl_hstar_hpure_l. intros H2.
false. math.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
