Solution for Rules.triple_set
intros. intros s1 K. lets ->: hsingle_inv K. applys eval_set.
{ applys* Fmap.indom_single. }
{ rewrite hstar_hpure_l. split*. rewrite Fmap.update_single.
applys hsingle_intro. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
