This avoids `naive_solver` tearing whole goals apart, even if the goal appears exactly as a hypothesis.