Solution for Hprop.HpropProofs.hstar_hpure_l
intros. apply propositional_extensionality. iff M.
{ hnf in M. destruct M as (h1&h2&M1&M2&D&U).
hnf in M1. destruct M1 as (M1&HP). subst.
rewrite Fmap.union_empty_l. auto. }
{ destruct M as (HP&Hh). hnf.
exists (Fmap.empty:heap) h. splits.
{ hnf. auto. }
{ auto. }
{ apply Fmap.disjoint_empty_l. }
{ rewrite Fmap.union_empty_l. auto. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
