[STATEMENT]
lemma sscan_shift[simp]: "sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)
[PROOF STEP]
by (induct xs arbitrary: a) (auto)