Managed to give a definition together with the required proves! :)
We use a helper function inside step, of which should be correct.
Next step is to maybe prove formally that it is still the same function.