Solution for Triples.BakedInFrame.btriple_frame
introv M. unfold triple in *. rename H' into H1. intros H2.
specializes M (H1 \* H2).
eapply hoare_conseq.
{ apply M. }
{ rewrite hstar_assoc. auto. }
{ intros v. rewrite hstar_assoc. auto. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
