Solution for Hprop.HpropProofs.hstar_hempty_l
intros. apply hprop_eq. split.
{ intros (h1&h2&M1&M2&D&U). hnf in M1. subst.
rewrite @Fmap.union_empty_l. auto. }
{ intros M. exists (Fmap.empty:heap) h. splits~.
{ hnf. auto. }
{ rewrite @Fmap.union_empty_l. auto. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
