-| #T1 #HT01 #HX #H destruct
- elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
- #T #HT1 #HT2 -L0 -V0 -W0 -T0
- elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HX) -T1 [| /3 width=1 by drops_refl, drops_drop/ ] #X0 #HXT #HX0
- /4 width=7 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/
+| #X0 #HXT0 #H1X0 #H destruct
+ lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0
+ elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
+ elim (cnv_cpm_conf_lpr_far … IH … H1X0 … HX02 … HL01 … HL02)
+ [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0
+ /4 width=8 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/