Add lemmas for creating later credits for non-pure steps (alternative)

This is an alternative to !1034 (closed).

Add twp_wp_step_lb and use that to prove steps_lb later credit lemmas for HeapLang atomic instructions.

I only derived the version for Alloc, but the others should be similar.

Let's first see if we like this approach better.