# [isabelle] Simple subgoal involving sets & lists

I have a theorem which I have reduced to the following subgoal (ignore
the first assumption, it's left over from another part of the proof) :
\<And>a thelist.
\<lbrakk>(\<forall>x. x \<in> set thelist \<Longrightarrow> x
\<in> G) \<Longrightarrow> prod_group thelist \<in> G;
\<forall>x. x \<in> set (a # thelist) \<Longrightarrow> x \<in>
G\<rbrakk>
\<Longrightarrow> a \<in> G
This looks quite provable to me.
If I apply( simp ), it reduces to:
\<And>a thelist.
\<lbrakk>(\<forall>x. x \<in> set thelist \<Longrightarrow> x
\<in> G) \<Longrightarrow> prod_group thelist \<in> G;
\<forall>x. x \<in> set (a # thelist) \<Longrightarrow> x \<in>
G\<rbrakk>
\<Longrightarrow> a \<in> G
which looks even more provable. However, I'm stuck. Anyone know what's
going on? Is this indeed unprovable because of a mistake I've made?
Thanks,
Matthew

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*