lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
[3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
- /4 width=7 by cnv_appl, minus_le_trans_sn/
+ /3 width=7 by cnv_appl, le_ylt_trans/
| #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
- /5 width=7 by cnv_appl, cnv_bind, minus_le_trans_sn/
+ /4 width=7 by cnv_appl, cnv_bind, le_ylt_trans/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1