--- a/Nominal/Ex/Let.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/Let.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -37,16 +37,6 @@
 is
   "permute_bn_raw"
 
-lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
-  apply (rule TrueI)+
-  apply simp_all
-  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
-  apply simp_all
-  done
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu: