Solution for Rules.LetFrame.triple_let_frame
introv M1 WH M2.
applys triple_conseq WH.
{ applys triple_let.
{ applys triple_frame. applys M1. }
{ applys M2. } }
{ applys qimpl_refl. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
