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
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