[STATEMENT]
lemma valid_lists_subset: "xs \<in> valid_lists S G \<Longrightarrow> set xs \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> valid_lists S G \<Longrightarrow> set xs \<subseteq> S
[PROOF STEP]
by (induction rule: valid_lists.induct) auto