[STATEMENT]
lemma fmap_ball_all4':
  fixes 
  Px :: "'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f \<Rightarrow> bool" and 
  P :: "'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f \<Rightarrow> 'b option \<Rightarrow> ('a::finite) \<Rightarrow> bool"
  assumes
  "\<forall>l\<in>dom (f::('a -~> 'b)). 
    \<forall>(x::'c) (y::'d) (z::'e) (a::'f). Px x y z a \<longrightarrow> P x y z a (f l) l"
  shows
  "\<forall>x y z a. Px x y z a \<longrightarrow> (\<forall>l\<in>dom f. P x y z a (f l) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z a. Px x y z a \<longrightarrow> (\<forall>l\<in>dom f. P x y z a (f l) l)
[PROOF STEP]
proof (intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
fix x y z a l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
assume "Px x y z a" and "l \<in> dom f"
[PROOF STATE]
proof (state)
this:
Px x y z a
l \<in> dom f

goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>dom f. \<forall>x y z a. Px x y z a \<longrightarrow> P x y z a (f l) l
Px x y z a
l \<in> dom f
[PROOF STEP]
show "P x y z a (f l) l"
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>dom f. \<forall>x y z a. Px x y z a \<longrightarrow> P x y z a (f l) l
Px x y z a
l \<in> dom f

goal (1 subgoal):
 1. P x y z a (f l) l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P x y z a (f l) l

goal:
No subgoals!
[PROOF STEP]
qed