--- a/Nominal/Ex/Let.thy	Mon Jun 20 08:50:13 2011 +0900
+++ b/Nominal/Ex/Let.thy	Mon Jun 20 09:29:42 2011 +0900
@@ -121,8 +121,7 @@
   by (simp add: permute_pure)
 
 (* TODO: should be provided by nominal *)
-lemma [eqvt]: "p \<bullet> bn a = bn (p \<bullet> a)"
-  by descending (rule eqvts)
+lemmas [eqvt] = trm_assn.fv_bn_eqvt
 
 (* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *)
 nominal_primrec
@@ -151,6 +150,7 @@
   apply (erule Abs_lst_fcb)
   apply (simp_all add: pure_fresh)
   apply (simp_all add: eqvt_at_def eqvts)
+  apply (rule arg_cong) back
   oops
 
 nominal_primrec