Introduce step relation, show equivalence

It is likely a better idea to use [step_rel] in the [iter] relation.