Solution for Rules.triple_free'
intros. intros s1 K. lets ->: hsingle_inv K. applys eval_free.
{ applys* Fmap.indom_single. }
{ rewrite* Fmap.remove_single. applys* hpure_intro. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
