/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →
/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →