Skip to content

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

tlsomers requested 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