Solution for Affine.NewTriples.triple_ramified_frame_hgc
introv M W. applys triple_conseq_frame_hgc (Q1 \--* (Q \*+ \GC)) M.
{ applys W. } { applys qwand_cancel. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
