Fix proof of lift_st