lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #X0 [3,6: #d0 ] #HK0 #HVX0 [1,2: #HX02 #H |3,5: #HX02 |4,6: #H1 #H2 ] destruct
lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #X0 [3,6: #d0 ] #HK0 #HVX0 [1,2: #HX02 #H |3,5: #HX02 |4,6: #H1 #H2 ] destruct
lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct