By induction on the lift. The combinators are handled by functoriality, and each atomic lift has a drop inverse by the isomorphism axioms; for $split$ the inverse is the concatenation map $unsplit$, and for $shift$ it is $⟨[], unshift⟩$.