Basic later credits implementation for HeapLang

This MR implements a basic version of later credits for HeapLang, providing lemmas for generating a) one credit for a pure step, or b) multiple credits if a persistent time receipt (steps_lb) is available.

It deliberately does not try to solve the following things:

• generate credits on non-pure steps, e.g. loads. This would require some re-engineering, because currently all of these lemmas are proved in terms of the corresponding lemmas for the total WP, which does not generate credits at all. But even getting credits for pure steps seems really useful already, since there's usually a beta-reduction around.
• add regeneration for credits as in the later credits paper. Since there are already persistent time receipts in HeapLang, which we likely want to stay compatible with, this would be a slightly larger addition. (I have got an implementation of the combination of persistent/cumulative receipts with later credits already for another project, so it can definitely be done, but there will probably some discussion about how exactly we want to do it for HeapLang.)
• add proof mode support, e.g. for a credit store that is managed by the proof tactics to keep credits around.

Input on this would be very welcome.

The current purestep lemmas are slightly unergonomic, because a separate done is often needed for the evaluation sidecondition (e.g. for binops). One way to make it more ergonomic would be to add variants of the wp_pure tactic for the two lemmas. Opinions on this?

CC @simonspies