[STATEMENT]
lemma visited_states_length : "length (visited_states q p) = Suc (length p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (visited_states q p) = Suc (length p)
[PROOF STEP]
by auto