[STATEMENT]
lemma nextElem_append[simp]:
 "y \<notin> set xs \<Longrightarrow> nextElem (xs @ ys) d y = nextElem ys d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> nextElem (xs @ ys) d y = nextElem ys d y
[PROOF STEP]
by(induct xs) auto