+| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
+ elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
+ >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
+ elim (ldrops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
+ elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
+ elim (lifts_lift_trans … HVW1 … HW12 … Hdes0) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
+ >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
+ @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/