[STATEMENT]
lemma infer_l_fresh:
  assumes  "\<turnstile> l \<Rightarrow> \<tau>"
  shows "atom x \<sharp> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
have "[] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
using wfG_nilI wfTh_emptyI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil 
   \<turnstile>\<^sub>w\<^sub>f [] 

goal (1 subgoal):
 1.  [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil 

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
hence "[] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>"
[PROOF STATE]
proof (prove)
using this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil 

goal (1 subgoal):
 1.  [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
using assms infer_l_wf
[PROOF STATE]
proof (prove)
using this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil 
 \<turnstile> l \<Rightarrow> \<tau>
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> 
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> 
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> 

goal (1 subgoal):
 1.  [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau> 

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau> 

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
using  fresh_def wfT_supp
[PROOF STATE]
proof (prove)
using this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau> 
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow> supp ?\<tau> \<subseteq> atom_dom ?\<Gamma> \<union> supp ?\<B>

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<tau>

goal:
No subgoals!
[PROOF STEP]
qed