--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -325,9 +325,6 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)"
-  by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt)
 
 lemma supp_fun_app2_eqvt:
   assumes e: "eqvt f"