proposition: Lemma lift_lift_reversed: forall `{Lift T}, LiftLift -> forall wk k ws s t, k >= s + ws -> lift wk k (lift ws s t) = lift ws s (lift wk (k - ws) t).
proof: Proof. intros. replace k with (ws + (k - ws)) by lia. erewrite <- lift_lift by lia. replace (ws + (k - ws) - ws) with (k - ws) by lia. reflexivity. Qed.
imports: Arith Lia Dblib.DblibTactics