elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
/2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide
#X #_ #H elim (lift_inv_lref2_be … H) -H //
elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
/2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide
#X #_ #H elim (lift_inv_lref2_be … H) -H //