[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
#K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
/4 width=7 by cpx_delta, fqu_drop, drop_drop, ex3_2_intro/
[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
#K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
/4 width=7 by cpx_delta, fqu_drop, drop_drop, ex3_2_intro/