Solution for Himpl.XsimplTactic.EntailmentProofs.himpl_example_1
intros. rewrite (hstar_comm (p3 ~~> 8) ((p2 ~~> 7) \* (p1 ~~> 6))).
rewrite (hstar_comm_assoc (p4 ~~> 9)).
rewrite (hstar_comm (p2 ~~> 7) (p1 ~~> 6)).
rewrite <- (hstar_assoc (p1 ~~> 6)).
apply himpl_frame_r. rewrite hstar_comm. apply himpl_refl.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
