[STATEMENT]
lemma nocross_UV_lists_subset:
  "{x. set x = X \<and> distinct x \<and> take 1 x = [r]
     \<and> no_cross_products (create_ldeep x) \<and> (\<forall>xs \<in> Y. sublist xs x)}
  \<subseteq> {x. set x = X \<and> distinct x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. set x = X \<and> distinct x \<and> take 1 x = [r] \<and> no_cross_products (create_ldeep x) \<and> (\<forall>xs\<in>Y. sublist xs x)} \<subseteq> {x. set x = X \<and> distinct x}
[PROOF STEP]
by blast