[STATEMENT]
lemma in_nlists_Suc_iff: "(xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> nlists n A. xs = y#ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys\<in>nlists n A. xs = y # ys)
[PROOF STEP]
unfolding nlists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> {xs. length xs = Suc n \<and> set xs \<subseteq> A}) = (\<exists>y\<in>A. \<exists>ys\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. xs = y # ys)
[PROOF STEP]
by (cases "xs") auto