src/HOL/Nominal/Examples/Weakening.thy

   have a1: "\<Gamma>1 \<lless> \<Gamma>2" by fact
   have a2: "valid \<Gamma>2" by fact
   have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp 
   moreover
   have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force
-  ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force
+  ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp 
   with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force
 qed (auto simp add: sub_def) (* app and var case *)
 
 text{* The original induction principle for typing 
        is not strong enough - so the simple proof fails *}