Solution for Hprop.HpropProofs.hstar_assoc
{ intros (h1&h'&M1&M2&D&U). destruct M2 as (h2&h3&M3&M4&D'&U').
subst h'. rewrite Fmap.disjoint_union_eq_r in D.
exists (h1 \u h2) h3. splits.
{ exists* h1 h2. }
{ apply M4. }
{ rewrite* @Fmap.disjoint_union_eq_l. }
{ rewrite* @Fmap.union_assoc. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
