| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=7 by cpxs_delta, cpxs_strap2/
|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=7 by cpxs_delta, cpxs_strap2/
|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/