- |#M #eqM #_ @(ex_intro … N) /2/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
+ |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
+ |3,4,5: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M1 #M2 #N1 #N2 #pr1 #pr2 #_ #_ #H destruct #eqP
+ @(ex_intro … M2) @(ex_intro … N2) /3/