Solution for Himpl.XsimplTactic.EntailmentProofs.himpl_example_3
intros. applys himpl_hexists_l. intros n.
rewrite hstar_comm. applys himpl_hstar_hpure_l. intros Hn.
applys himpl_hexists_r (n+1). applys himpl_hstar_hpure_r.
{ math. } { math_rewrite (n+1-1 = n). applys himpl_refl. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
