elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0
/3 width=7 by cnv_appl_cpes, or_introl/
(* Note: argument type mismatch *)
| @or_intror #H -n
elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX
elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0
/3 width=7 by cnv_appl_cpes, or_introl/
(* Note: argument type mismatch *)
| @or_intror #H -n
elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX