Solution for Himpl.EntailmentRulesProofs.himpl_frame_lr
introv M1 M2. applys himpl_trans.
{ applys himpl_frame_l. applys M1. }
{ applys himpl_frame_r. applys M2. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback