/3 width=5 by drops_isuni_fwd_drop2, frees_sort_pushs/
| #f1 #I #K #V #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
lapply (isfin_inv_next … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
lapply (lifts_inv_lref1 … H2) -H2 * #j #Hf #H destruct
elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #HVW
/3 width=5 by drops_isuni_fwd_drop2, frees_sort_pushs/
| #f1 #I #K #V #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
lapply (isfin_inv_next … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
lapply (lifts_inv_lref1 … H2) -H2 * #j #Hf #H destruct
elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #HVW