lapply (drops_tls_at … Hf … HY) -HY #HY
elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK0 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #W1 #HVW1 #H destruct
elim (lifts_total W1 (𝐔❨↑j❩)) #W2 #HW12
lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
lapply (drops_tls_at … Hf … HY) -HY #HY
elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK0 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #W1 #HVW1 #H destruct
elim (lifts_total W1 (𝐔❨↑j❩)) #W2 #HW12
lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H