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.
Edited by Robbert Krebbers