[STATEMENT]
lemma nextElem_notin_butlast[rule_format,simp]:
 "y \<notin> set(butlast xs) \<longrightarrow> nextElem xs x y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> set (butlast xs) \<longrightarrow> nextElem xs x y = x
[PROOF STEP]
by(induct xs) auto