[STATEMENT]
lemma list_all2_leftE:
  assumes "list_all2 P xs ys" "x \<in> set xs"
  obtains y where "y \<in> set ys" "P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set ys; P x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 P xs ys
x \<in> set xs

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set ys; P x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by induct auto