[STATEMENT]
lemma deriv_psubst:
  fixes f :: \<open>'a \<Rightarrow> 'a\<close>
  assumes inf_params: \<open>infinite (UNIV :: 'a set)\<close>
  shows \<open>z \<turnstile> p \<Longrightarrow> map (psubst f) z \<turnstile> psubst f p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<turnstile> p \<Longrightarrow> map (psubst f) z \<turnstile> psubst f p
[PROOF STEP]
proof (induct z p arbitrary: f rule: deriv.induct)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>a G f. a \<in> set G \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>G f. map (psubst f) G \<turnstile> psubst f TT
 3. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 5. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 6. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 7. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 9. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 10. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
A total of 18 subgoals...
[PROOF STEP]
case (Assum a G)
[PROOF STATE]
proof (state)
this:
a \<in> set G

goal (18 subgoals):
 1. \<And>a G f. a \<in> set G \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>G f. map (psubst f) G \<turnstile> psubst f TT
 3. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 5. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 6. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 7. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 9. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 10. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> set G

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
using deriv.Assum member_psubst
[PROOF STATE]
proof (prove)
using this:
a \<in> set G
?a \<in> set ?G \<Longrightarrow> ?G \<turnstile> ?a
?p \<in> set ?z \<Longrightarrow> psubst ?f ?p \<in> set (map (psubst ?f) ?z)

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f a

goal (17 subgoals):
 1. \<And>G f. map (psubst f) G \<turnstile> psubst f TT
 2. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 4. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 5. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 8. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>G f. map (psubst f) G \<turnstile> psubst f TT
 2. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 4. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 5. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 8. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
A total of 17 subgoals...
[PROOF STEP]
case (TTI G)
[PROOF STATE]
proof (state)
this:

goal (17 subgoals):
 1. \<And>G f. map (psubst f) G \<turnstile> psubst f TT
 2. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 4. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 5. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 8. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f TT
[PROOF STEP]
using deriv.TTI
[PROOF STATE]
proof (prove)
using this:
?G \<turnstile> TT

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f TT
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f TT

goal (16 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 3. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 4. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 8. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 3. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 4. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 8. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
A total of 16 subgoals...
[PROOF STEP]
case (FFE G a)
[PROOF STATE]
proof (state)
this:
G \<turnstile> FF
map (psubst ?f) G \<turnstile> psubst ?f FF

goal (16 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> FF; \<And>f. map (psubst f) G \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 3. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 4. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 7. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 8. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 10. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
A total of 16 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> FF
map (psubst ?f) G \<turnstile> psubst ?f FF
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> FF
map (psubst ?f) G \<turnstile> psubst ?f FF

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
using deriv.FFE
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> FF
map (psubst ?f) G \<turnstile> psubst ?f FF
?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f a

goal (15 subgoals):
 1. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 2. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 3. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 7. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 10. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 2. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 3. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 7. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 10. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
A total of 15 subgoals...
[PROOF STEP]
case (NegI a G)
[PROOF STATE]
proof (state)
this:
a # G \<turnstile> FF
map (psubst ?f) (a # G) \<turnstile> psubst ?f FF

goal (15 subgoals):
 1. \<And>a G f. \<lbrakk>a # G \<turnstile> FF; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Neg a)
 2. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 3. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 6. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 7. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 9. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 10. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
A total of 15 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a # G \<turnstile> FF
map (psubst ?f) (a # G) \<turnstile> psubst ?f FF
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a # G \<turnstile> FF
map (psubst ?f) (a # G) \<turnstile> psubst ?f FF

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Neg a)
[PROOF STEP]
using deriv.NegI
[PROOF STATE]
proof (prove)
using this:
a # G \<turnstile> FF
map (psubst ?f) (a # G) \<turnstile> psubst ?f FF
?a # ?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> Neg ?a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Neg a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f (Neg a)

goal (14 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 2. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 9. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 10. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 2. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 9. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 10. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
A total of 14 subgoals...
[PROOF STEP]
case (NegE G a)
[PROOF STATE]
proof (state)
this:
G \<turnstile> Neg a
map (psubst ?f) G \<turnstile> psubst ?f (Neg a)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (14 subgoals):
 1. \<And>G a f. \<lbrakk>G \<turnstile> Neg a; \<And>f. map (psubst f) G \<turnstile> psubst f (Neg a); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f FF
 2. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 5. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 6. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 8. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 9. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 10. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> Neg a
map (psubst ?f) G \<turnstile> psubst ?f (Neg a)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Neg a
map (psubst ?f) G \<turnstile> psubst ?f (Neg a)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f FF
[PROOF STEP]
using deriv.NegE
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Neg a
map (psubst ?f) G \<turnstile> psubst ?f (Neg a)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
\<lbrakk>?G \<turnstile> Neg ?a; ?G \<turnstile> ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> FF

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f FF
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f FF

goal (13 subgoals):
 1. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 8. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 9. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 10. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 8. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 9. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 10. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
A total of 13 subgoals...
[PROOF STEP]
case (Class a G)
[PROOF STATE]
proof (state)
this:
Neg a # G \<turnstile> FF
map (psubst ?f) (Neg a # G) \<turnstile> psubst ?f FF

goal (13 subgoals):
 1. \<And>a G f. \<lbrakk>Neg a # G \<turnstile> FF; \<And>f. map (psubst f) (Neg a # G) \<turnstile> psubst f FF\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 2. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 4. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 5. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 7. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 8. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 9. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 10. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
A total of 13 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg a # G \<turnstile> FF
map (psubst ?f) (Neg a # G) \<turnstile> psubst ?f FF
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Neg a # G \<turnstile> FF
map (psubst ?f) (Neg a # G) \<turnstile> psubst ?f FF

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
using deriv.Class
[PROOF STATE]
proof (prove)
using this:
Neg a # G \<turnstile> FF
map (psubst ?f) (Neg a # G) \<turnstile> psubst ?f FF
Neg ?a # ?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f a

goal (12 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 10. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 10. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
A total of 12 subgoals...
[PROOF STEP]
case (ImplE G a b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> Impl a b
map (psubst ?f) G \<turnstile> psubst ?f (Impl a b)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (12 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 10. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> Impl a b
map (psubst ?f) G \<turnstile> psubst ?f (Impl a b)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
[PROOF STEP]
have \<open>map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b)\<close>
    and \<open>map (psubst f) G \<turnstile> psubst f a\<close>
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Impl a b
map (psubst ?f) G \<turnstile> psubst ?f (Impl a b)
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b) &&& map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b)
map (psubst f) G \<turnstile> psubst f a

goal (12 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a b f. \<lbrakk>G \<turnstile> Impl a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Impl a b); G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 9. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 10. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b)
map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b)
map (psubst f) G \<turnstile> psubst f a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
using deriv.ImplE
[PROOF STATE]
proof (prove)
using this:
map (psubst f) G \<turnstile> Impl (psubst f a) (psubst f b)
map (psubst f) G \<turnstile> psubst f a
\<lbrakk>?G \<turnstile> Impl ?a ?b; ?G \<turnstile> ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f b

goal (11 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 9. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 10. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 9. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 10. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
A total of 11 subgoals...
[PROOF STEP]
case (ImplI G a b)
[PROOF STATE]
proof (state)
this:
G # a \<turnstile> b
map (psubst ?f) (G # a) \<turnstile> psubst ?f b

goal (11 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>a G b f. \<lbrakk>a # G \<turnstile> b; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Impl a b)
 8. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 9. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 10. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G # a \<turnstile> b
map (psubst ?f) (G # a) \<turnstile> psubst ?f b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G # a \<turnstile> b
map (psubst ?f) (G # a) \<turnstile> psubst ?f b

goal (1 subgoal):
 1. map (psubst f) a \<turnstile> psubst f (Impl G b)
[PROOF STEP]
using deriv.ImplI
[PROOF STATE]
proof (prove)
using this:
G # a \<turnstile> b
map (psubst ?f) (G # a) \<turnstile> psubst ?f b
?a # ?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Impl ?a ?b

goal (1 subgoal):
 1. map (psubst f) a \<turnstile> psubst f (Impl G b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) a \<turnstile> psubst f (Impl G b)

goal (10 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 8. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 9. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 10. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 8. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 9. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 10. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (OrE G a b c)
[PROOF STATE]
proof (state)
this:
G \<turnstile> Or a b
map (psubst ?f) G \<turnstile> psubst ?f (Or a b)
a # G \<turnstile> c
map (psubst ?f) (a # G) \<turnstile> psubst ?f c
b # G \<turnstile> c
map (psubst ?f) (b # G) \<turnstile> psubst ?f c

goal (10 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 8. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 9. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 10. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> Or a b
map (psubst ?f) G \<turnstile> psubst ?f (Or a b)
a # G \<turnstile> c
map (psubst ?f) (a # G) \<turnstile> psubst ?f c
b # G \<turnstile> c
map (psubst ?f) (b # G) \<turnstile> psubst ?f c
[PROOF STEP]
have \<open>map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b)\<close>
    and \<open>psubst f a # map (psubst f) G \<turnstile> psubst f c\<close>
    and \<open>psubst f b # map (psubst f) G \<turnstile> psubst f c\<close>
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Or a b
map (psubst ?f) G \<turnstile> psubst ?f (Or a b)
a # G \<turnstile> c
map (psubst ?f) (a # G) \<turnstile> psubst ?f c
b # G \<turnstile> c
map (psubst ?f) (b # G) \<turnstile> psubst ?f c

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b) &&& psubst f a # map (psubst f) G \<turnstile> psubst f c &&& psubst f b # map (psubst f) G \<turnstile> psubst f c
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b)
psubst f a # map (psubst f) G \<turnstile> psubst f c
psubst f b # map (psubst f) G \<turnstile> psubst f c

goal (10 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a b c f. \<lbrakk>G \<turnstile> Or a b; \<And>f. map (psubst f) G \<turnstile> psubst f (Or a b); a # G \<turnstile> c; \<And>f. map (psubst f) (a # G) \<turnstile> psubst f c; b # G \<turnstile> c; \<And>f. map (psubst f) (b # G) \<turnstile> psubst f c\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f c
 7. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 8. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 9. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 10. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b)
psubst f a # map (psubst f) G \<turnstile> psubst f c
psubst f b # map (psubst f) G \<turnstile> psubst f c
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b)
psubst f a # map (psubst f) G \<turnstile> psubst f c
psubst f b # map (psubst f) G \<turnstile> psubst f c

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f c
[PROOF STEP]
using deriv.OrE
[PROOF STATE]
proof (prove)
using this:
map (psubst f) G \<turnstile> Or (psubst f a) (psubst f b)
psubst f a # map (psubst f) G \<turnstile> psubst f c
psubst f b # map (psubst f) G \<turnstile> psubst f c
\<lbrakk>?G \<turnstile> Or ?a ?b; ?a # ?G \<turnstile> ?c; ?b # ?G \<turnstile> ?c\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?c

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f c

goal (9 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 7. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 8. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 9. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 7. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 8. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 9. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (OrI1 G a b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (9 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 6. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 7. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 8. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 9. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Or a b)
[PROOF STEP]
using deriv.OrI1
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
?G \<turnstile> ?a \<Longrightarrow> ?G \<turnstile> Or ?a ?b

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Or a b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f (Or a b)

goal (8 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 6. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 7. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 8. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 6. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 7. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 8. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (OrI2 G a b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (8 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G b a f. \<lbrakk>G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Or a b)
 5. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 6. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 7. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 8. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Or b a)
[PROOF STEP]
using deriv.OrI2
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Or ?a ?b

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (Or b a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f (Or b a)

goal (7 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 5. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 6. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 7. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 5. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 6. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 7. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (AndE1 G a b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> And a b
map (psubst ?f) G \<turnstile> psubst ?f (And a b)

goal (7 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f a
 3. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 4. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 5. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 6. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 7. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> And a b
map (psubst ?f) G \<turnstile> psubst ?f (And a b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> And a b
map (psubst ?f) G \<turnstile> psubst ?f (And a b)

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
using deriv.AndE1
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> And a b
map (psubst ?f) G \<turnstile> psubst ?f (And a b)
?G \<turnstile> And ?a ?b \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f a

goal (6 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 3. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 4. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 5. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 6. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 3. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 4. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 5. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 6. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (AndE2 p q z)
[PROOF STATE]
proof (state)
this:
p \<turnstile> And q z
map (psubst ?f) p \<turnstile> psubst ?f (And q z)

goal (6 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a b f. \<lbrakk>G \<turnstile> And a b; \<And>f. map (psubst f) G \<turnstile> psubst f (And a b)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
 3. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 4. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 5. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 6. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<turnstile> And q z
map (psubst ?f) p \<turnstile> psubst ?f (And q z)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> And q z
map (psubst ?f) p \<turnstile> psubst ?f (And q z)

goal (1 subgoal):
 1. map (psubst f) p \<turnstile> psubst f z
[PROOF STEP]
using deriv.AndE2
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> And q z
map (psubst ?f) p \<turnstile> psubst ?f (And q z)
?G \<turnstile> And ?a ?b \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. map (psubst f) p \<turnstile> psubst f z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) p \<turnstile> psubst f z

goal (5 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 3. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 4. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 5. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 3. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 4. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 5. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (AndI G a b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
G \<turnstile> b
map (psubst ?f) G \<turnstile> psubst ?f b

goal (5 subgoals):
 1. \<And>G a b f. \<lbrakk>G \<turnstile> a; \<And>f. map (psubst f) G \<turnstile> psubst f a; G \<turnstile> b; \<And>f. map (psubst f) G \<turnstile> psubst f b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (And a b)
 2. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 3. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 4. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 5. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
G \<turnstile> b
map (psubst ?f) G \<turnstile> psubst ?f b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
G \<turnstile> b
map (psubst ?f) G \<turnstile> psubst ?f b

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (And a b)
[PROOF STEP]
using deriv.AndI
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a
map (psubst ?f) G \<turnstile> psubst ?f a
G \<turnstile> b
map (psubst ?f) G \<turnstile> psubst ?f b
\<lbrakk>?G \<turnstile> ?a; ?G \<turnstile> ?b\<rbrakk> \<Longrightarrow> ?G \<turnstile> And ?a ?b

goal (1 subgoal):
 1. map (psubst f) G \<turnstile> psubst f (And a b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
map (psubst f) G \<turnstile> psubst f (And a b)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
case (ExistsE z p c q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
let ?params = \<open>params p \<union> params q \<union> (\<Union>p \<in> set z. params p)\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
have \<open>finite ?params\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (params p \<union> params q \<union> \<Union> (params ` set z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (params p \<union> params q \<union> \<Union> (params ` set z))

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (params p \<union> params q \<union> \<Union> (params ` set z))
[PROOF STEP]
obtain fresh where *: \<open>fresh \<notin> ?params \<union> {c} \<union> image f ?params\<close>
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> params q \<union> \<Union> (params ` set z))

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> params q \<union> \<Union> (params ` set z)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_new_if_finite inf_params
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> params q \<union> \<Union> (params ` set z))
\<lbrakk>infinite UNIV; finite ?A\<rbrakk> \<Longrightarrow> \<exists>a. a \<notin> ?A
infinite UNIV

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> params q \<union> \<Union> (params ` set z)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite.emptyI finite.insertI finite_UnI finite_imageI)
[PROOF STATE]
proof (state)
this:
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> params q \<union> \<Union> (params ` set z))

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
let ?f = \<open>f(c := fresh)\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
have \<open>news c (p # q # z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c (p # q # z)
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q

goal (1 subgoal):
 1. news c (p # q # z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news c (p # q # z)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c (p # q # z)
[PROOF STEP]
have \<open>new fresh (psubst ?f p)\<close> \<open>new fresh (psubst ?f q)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
news c (p # q # z)

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& new fresh (psubst (f(c := fresh)) q) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
using * new_psubst_image news_psubst
[PROOF STATE]
proof (prove)
using this:
news c (p # q # z)
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> params q \<union> \<Union> (params ` set z))
\<lbrakk>new ?c ?p; ?d \<notin> ?f ` params ?p\<rbrakk> \<Longrightarrow> new ?d (psubst (?f(?c := ?d)) ?p)
\<lbrakk>news ?c ?z; ?d \<notin> ?f ` \<Union> (params ` set ?z)\<rbrakk> \<Longrightarrow> news ?d (map (psubst (?f(?c := ?d))) ?z)

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& new fresh (psubst (f(c := fresh)) q) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
by (fastforce simp add: image_Un)+
[PROOF STATE]
proof (state)
this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
have \<open>map (psubst ?f) z = map (psubst f) z\<close>
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z = map (psubst f) z
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z = map (psubst f) z
[PROOF STEP]
by (metis (mono_tags, lifting) Ball_set map_eq_conv psubst_upd)
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z = map (psubst f) z

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> psubst ?f (Exists p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (Exists p)
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (Exists p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (Exists p)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (Exists p)
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> Exists (psubst ?f p)\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (Exists p)

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
have \<open>map (psubst ?f) (subst p (App c []) 0 # z) \<turnstile> psubst ?f q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst (f(c := fresh))) (p[App c []/0] # z) \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) (p[App c []/0] # z) \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) (p[App c []/0] # z) \<turnstile> psubst (f(c := fresh)) q

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) (p[App c []/0] # z) \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
have \<open>subst (psubst ?f p) (App fresh []) 0 # map (psubst ?f) z \<turnstile> psubst ?f q\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) (p[App c []/0] # z) \<turnstile> psubst (f(c := fresh)) q

goal (1 subgoal):
 1. psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
have \<open>news fresh (map (psubst ?f) (p # q # z))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news fresh (map (psubst (f(c := fresh))) (p # q # z))
[PROOF STEP]
using \<open>new fresh (psubst ?f p)\<close> \<open>new fresh (psubst ?f q)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. news fresh (map (psubst (f(c := fresh))) (p # q # z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news fresh (map (psubst (f(c := fresh))) (p # q # z))

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news fresh (map (psubst (f(c := fresh))) (p # q # z))
[PROOF STEP]
have \<open>new fresh (psubst ?f p)\<close> \<open>new fresh (psubst ?f q)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
news fresh (map (psubst (f(c := fresh))) (p # q # z))

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& new fresh (psubst (f(c := fresh)) q) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)
psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> psubst ?f q\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)
psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
using deriv.ExistsE
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> Exists (psubst (f(c := fresh)) p)
psubst (f(c := fresh)) p[App fresh []/0] # map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
new fresh (psubst (f(c := fresh)) p)
new fresh (psubst (f(c := fresh)) q)
news fresh (map (psubst (f(c := fresh))) z)
\<lbrakk>?G \<turnstile> Exists ?a; ?a[App ?n []/0] # ?G \<turnstile> ?b; news ?n ?G; new ?n ?a; new ?n ?b\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q

goal (4 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
 4. \<And>G a n b f. \<lbrakk>G \<turnstile> Exists a; \<And>f. map (psubst f) G \<turnstile> psubst f (Exists a); a[App n []/0] # G \<turnstile> b; \<And>f. map (psubst f) (a[App n []/0] # G) \<turnstile> psubst f b; news n G; new n a; new n b\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f q
[PROOF STEP]
using ExistsE \<open>map (psubst ?f) z = map (psubst f) z\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) q
z \<turnstile> Exists p
map (psubst ?f) z \<turnstile> psubst ?f (Exists p)
p[App c []/0] # z \<turnstile> q
map (psubst ?f) (p[App c []/0] # z) \<turnstile> psubst ?f q
news c z
new c p
new c q
map (psubst (f(c := fresh))) z = map (psubst f) z

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (psubst f) z \<turnstile> psubst f q

goal (3 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
[PROOF STEP]
case (ExistsI z p t)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p[t/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[t/0])

goal (3 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
 3. \<And>G a t f. \<lbrakk>G \<turnstile> a[t/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[t/0])\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Exists a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> p[t/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[t/0])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[t/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[t/0])

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (Exists p)
[PROOF STEP]
using deriv.ExistsI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[t/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[t/0])
?G \<turnstile> ?a[?t/0] \<Longrightarrow> ?G \<turnstile> Exists ?a

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (Exists p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) z \<turnstile> psubst f (Exists p)

goal (2 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
[PROOF STEP]
case (ForallE z p t)
[PROOF STATE]
proof (state)
this:
z \<turnstile> Forall p
map (psubst ?f) z \<turnstile> psubst ?f (Forall p)

goal (2 subgoals):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
 2. \<And>G a t f. \<lbrakk>G \<turnstile> Forall a; \<And>f. map (psubst f) G \<turnstile> psubst f (Forall a)\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (a[t/0])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> Forall p
map (psubst ?f) z \<turnstile> psubst ?f (Forall p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Forall p
map (psubst ?f) z \<turnstile> psubst ?f (Forall p)

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (p[t/0])
[PROOF STEP]
using deriv.ForallE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Forall p
map (psubst ?f) z \<turnstile> psubst ?f (Forall p)
?G \<turnstile> Forall ?a \<Longrightarrow> ?G \<turnstile> ?a[?t/0]

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (p[t/0])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (psubst f) z \<turnstile> psubst f (p[t/0])

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
case (ForallI z p c)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p[App c []/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[App c []/0])
news c z
new c p

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
let ?params = \<open>params p \<union>(\<Union>p \<in> set z. params p)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
have \<open>finite ?params\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (params p \<union> \<Union> (params ` set z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (params p \<union> \<Union> (params ` set z))

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (params p \<union> \<Union> (params ` set z))
[PROOF STEP]
obtain fresh where *: \<open>fresh \<notin> ?params \<union> {c} \<union> image f ?params\<close>
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> \<Union> (params ` set z))

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> \<Union> (params ` set z)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_new_if_finite inf_params
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> \<Union> (params ` set z))
\<lbrakk>infinite UNIV; finite ?A\<rbrakk> \<Longrightarrow> \<exists>a. a \<notin> ?A
infinite UNIV

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> \<Union> (params ` set z)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite.emptyI finite.insertI finite_UnI finite_imageI)
[PROOF STATE]
proof (state)
this:
fresh \<notin> params p \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> \<Union> (params ` set z))

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
let ?f = \<open>f(c := fresh)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
have \<open>news c (p # z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c (p # z)
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[App c []/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[App c []/0])
news c z
new c p

goal (1 subgoal):
 1. news c (p # z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news c (p # z)

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c (p # z)
[PROOF STEP]
have \<open>new fresh (psubst ?f p)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
news c (p # z)

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
using * new_psubst_image news_psubst
[PROOF STATE]
proof (prove)
using this:
news c (p # z)
fresh \<notin> params p \<union> \<Union> (params ` set z) \<union> {c} \<union> f ` (params p \<union> \<Union> (params ` set z))
\<lbrakk>new ?c ?p; ?d \<notin> ?f ` params ?p\<rbrakk> \<Longrightarrow> new ?d (psubst (?f(?c := ?d)) ?p)
\<lbrakk>news ?c ?z; ?d \<notin> ?f ` \<Union> (params ` set ?z)\<rbrakk> \<Longrightarrow> news ?d (map (psubst (?f(?c := ?d))) ?z)

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
by (fastforce simp add: image_Un)+
[PROOF STATE]
proof (state)
this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
have \<open>map (psubst ?f) z = map (psubst f) z\<close>
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z = map (psubst f) z
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)
z \<turnstile> p[App c []/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[App c []/0])
news c z
new c p

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z = map (psubst f) z
[PROOF STEP]
by (metis (mono_tags, lifting) Ball_set map_eq_conv psubst_upd)
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z = map (psubst f) z

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> psubst ?f (subst p (App c []) 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (p[App c []/0])
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[App c []/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[App c []/0])
news c z
new c p

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (p[App c []/0])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (p[App c []/0])

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (p[App c []/0])
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> subst (psubst ?f p) (App fresh []) 0\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) (p[App c []/0])

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
have \<open>news fresh (map (psubst ?f) (p # z))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news fresh (map (psubst (f(c := fresh))) (p # z))
[PROOF STEP]
using \<open>new fresh (psubst ?f p)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. news fresh (map (psubst (f(c := fresh))) (p # z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news fresh (map (psubst (f(c := fresh))) (p # z))

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news fresh (map (psubst (f(c := fresh))) (p # z))
[PROOF STEP]
have \<open>new fresh (psubst ?f p)\<close> \<open>news fresh (map (psubst ?f) z)\<close>
[PROOF STATE]
proof (prove)
using this:
news fresh (map (psubst (f(c := fresh))) (p # z))

goal (1 subgoal):
 1. new fresh (psubst (f(c := fresh)) p) &&& news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)
[PROOF STEP]
have \<open>map (psubst ?f) z \<turnstile> Forall (psubst ?f p)\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)
[PROOF STEP]
using deriv.ForallI
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> psubst (f(c := fresh)) p[App fresh []/0]
new fresh (psubst (f(c := fresh)) p)
news fresh (map (psubst (f(c := fresh))) z)
\<lbrakk>?G \<turnstile> ?a[App ?n []/0]; news ?n ?G; new ?n ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> Forall ?a

goal (1 subgoal):
 1. map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)

goal (1 subgoal):
 1. \<And>G a n f. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>f. map (psubst f) G \<turnstile> psubst f (a[App n []/0]); news n G; new n a\<rbrakk> \<Longrightarrow> map (psubst f) G \<turnstile> psubst f (Forall a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (Forall p)
[PROOF STEP]
using ForallI \<open>map (psubst ?f) z = map (psubst f) z\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (f(c := fresh))) z \<turnstile> Forall (psubst (f(c := fresh)) p)
z \<turnstile> p[App c []/0]
map (psubst ?f) z \<turnstile> psubst ?f (p[App c []/0])
news c z
new c p
map (psubst (f(c := fresh))) z = map (psubst f) z

goal (1 subgoal):
 1. map (psubst f) z \<turnstile> psubst f (Forall p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (psubst f) z \<turnstile> psubst f (Forall p)

goal:
No subgoals!
[PROOF STEP]
qed