∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
#f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
#f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1