[STATEMENT]
lemma wfT_restrict2:
  fixes \<tau>::\<tau>
  assumes "wfT \<Theta> \<B> ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<tau>" and "atom x \<sharp> \<tau>" 
  shows "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
using wf_restrict1(4)[of \<Theta> \<B> "((x, b, c) #\<^sub>\<Gamma> \<Gamma>)"  \<tau> GNil x "b" "c" \<Gamma>] assms fresh_GNil append_g.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta> ; \<B> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> = GNil @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>; atom x \<sharp> \<tau>; atom x \<sharp> GNil\<rbrakk> \<Longrightarrow>  \<Theta> ; \<B> ; GNil @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau> 
 \<Theta> ; \<B> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau> 
atom x \<sharp> \<tau>
?a \<sharp> GNil
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
by auto