Solution for Affine.NewTriples.mkstruct_haffine_post
introv K. applys himpl_trans. 2: { applys mkstruct_hgc. }
applys mkstruct_conseq. xsimpl. applys himpl_hgc_r K.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback