There are real difficulties here, and you're right to point them out. But I'd nonetheless posit that staying within a simple logic as much as possible, and only rarely resorting to "powerful" proof steps such as a switch to a different reasoning approach, is very different from what most current ATP systems do. (Though it's closer to how custom "tactics" might be used in ITP. Which intersects in interesting ways with the question of whether current ITP sketches are "intuitive" enough to humans.)