Add lemmas for creating later credits for non-pure steps.

Thomas Somersrequested to merge
tlsomers/iris:later-credit-step-non-pure into master

Add versions of the wp stepping lemmas which additionally produce later credits.

Merge request reports