lapply (ldrop_mono … H … HLK1) -H #H destruct
elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
lapply (ldrop_mono … H … HLK1) -H #H destruct
elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct