Add later credits to the WP

This adds later credits to the weakest precondition, while keeping the step_fupdN for backwards compatibility.

Points that may be worth discussing:

• also the _no_lc versions of the fupd soundness lemmas now generate m initial credits (which are of course useless), in order to be able to supply the credits needed even in the _no_lc versions of the adequacy proof.
• it is not quite clear to me what the best way to update the lifting lemmas is. Not everyone needs credits, and just adding them there would probably create a lot of (easy-to-fix) breakage in all developments defining their own language instance. Currently, I've just kept the existing lemmas and added new ones suffixed with _lc where it makes sense.

All credit goes to @simonspies, of course.