[STATEMENT]
lemma first_tail_second: "first(tail s) = second s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first (tail s) = second s
[PROOF STEP]
by (simp add: first_def second_def tail_def suffix_def)