[STATEMENT]
lemma IF2wit: "x \<in> IF2set IF2wit \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> IF2set IF2wit \<Longrightarrow> False
[PROOF STEP]
unfolding IF2wit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> IF2set (ctor2 wit_F2) \<Longrightarrow> False
[PROOF STEP]
by (elim UnE F2.wit[elim_format] UN_E FalseE |
      rule refl |  hypsubst | assumption | unfold IF2set_simps)+