intros. apply himpl_antisym.
{ intros h K. applys hexists_intro h.
rewrite hstar_hpure_l. auto. }
{ applys himpl_hexists_l. intros h.
applys himpl_hstar_hpure_l. intros K.
intros h' E. subst. auto. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
