| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H
elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct
/5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/
| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H
elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct
/5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/