Round-six lemma `axSteps_at`