#L1 #L2 #U #d #HL12 #Hd @and3_intro // -HL12
#I1 #I2 #I #K1 #K2 #K #W1 #W2 #W #i #HLK1 #_ #HLK -L2 -K2
lapply (ldrop_mono … HLK … HLK1) -HLK #H destruct
#L1 #L2 #U #d #HL12 #Hd @and3_intro // -HL12
#I1 #I2 #I #K1 #K2 #K #W1 #W2 #W #i #HLK1 #_ #HLK -L2 -K2
lapply (ldrop_mono … HLK … HLK1) -HLK #H destruct