[STATEMENT]
lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)
[PROOF STEP]
by (auto simp add: prefix_def)