Use [step_rel] in [iter]

It was surprisingly easy. I expected a lot more proofs not to work.
Fixup proofs