|2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
lapply (ldrop_mono … H … HLK1) -H #H destruct
lapply (fsupp_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -V2
|2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
lapply (ldrop_mono … H … HLK1) -H #H destruct
lapply (fsupp_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -V2