[STATEMENT]
lemma F2set3_JF2set_incl_JF2set:
  "a' \<in> F2set3 (dtor2 a) \<Longrightarrow> JF2set a' \<subseteq> JF2set a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<in> F2set3 (dtor2 a) \<Longrightarrow> JF2set a' \<subseteq> JF2set a
[PROOF STEP]
apply (rule UN_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV\<rbrakk> \<Longrightarrow> JF2col n a' \<subseteq> JF2set a
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2set a
[PROOF STEP]
apply (rule UN_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> ?a4 n x \<in> UNIV
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?a4 n x) a
[PROOF STEP]
apply (rule UNIV_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?a4 n x) a
[PROOF STEP]
apply (rule subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> ?A8 n x \<subseteq> JF2col (?a4 n x) a
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> ?A8 n x
[PROOF STEP]
apply (rule equalityD2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> JF2col (?a4 n x) a = ?A8 n x
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> ?A8 n x
[PROOF STEP]
apply (rule JF2col_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> F2set1 (dtor2 a) \<union> (\<Union> (JF1col (?n13 n x) ` F2set2 (dtor2 a)) \<union> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a)))
[PROOF STEP]
apply (rule UnI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> \<Union> (JF1col (?n13 n x) ` F2set2 (dtor2 a)) \<union> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a))
[PROOF STEP]
apply (tactic \<open>rtac @{context} (BNF_Util.mk_UnIN  2 2) 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a))
[PROOF STEP]
apply (erule UN_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?n13 n x) a'
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done