Added capability for stripping multiple laters per step in HeapLang

In !595 (merged) the Iris program logic was extended with capability for stripping an amount of laters per step relative to the amount of steps taking thus far.

This was, however, never ported to HeapLang. It was instead instantiated with the constant function λ _, 0, retaining the original functionality of the language.

This MR seeks to add this functionality by:

• Adding a monotonically increasing number to the state interpretation (and ghost functor) of HeapLang
• Adding non-invasive lemmas that lets the user interact with this number by
  • Obtaining a new lower bound steps_lb 0 in the presence of any wp (via wp_lb_init)
  • Incrementing an existing lower bound steps_lb n to steps_lb (S n) when taking a step (via wp_lb_update)
  • Derive propositions P guarded under a number of laters relative to an existing lower bound steps_lb n (via wp_step_fupdN_lb).

The following formal rules summarises the idea in Hoare Triple notation (OBS: lemma names differ): The usefulness of this functionality is illustrated here: actris!26 (merged)

In particular, we previously had to use a skipN instruction within a lock to strip an amount of laters relative to the physical state. With this change we can instead track this amount in the logic, and strip all of the necessary laters.

The change seems entirely non-invasive, seeing that all user-level specifications remain intact.

EDIT: Thanks to @lgaeher for suggesting the more general theorem for total adequacy, which let me bump the total adequacy theorem of HeapLang