>(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
>(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