--- a/Nominal-General/Nominal2_Base.thy	Fri Apr 30 14:21:18 2010 +0100
+++ b/Nominal-General/Nominal2_Base.thy	Fri Apr 30 15:34:26 2010 +0100
@@ -1067,10 +1067,17 @@
   unfolding fresh_def supp_def 
   unfolding MOST_iff_cofinite by simp
 
+lemma supp_subset_fresh:
+  assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
+  shows "supp y \<subseteq> supp x"
+  using a
+  unfolding fresh_def
+  by blast
+
 lemma fresh_fun_app:
   assumes "a \<sharp> f" and "a \<sharp> x" 
   shows "a \<sharp> f x"
-  using assms 
+  using assms
   unfolding fresh_conv_MOST
   unfolding permute_fun_app_eq 
   by (elim MOST_rev_mp, simp)
@@ -1081,22 +1088,22 @@
   unfolding fresh_def
   by auto
 
+text {* support of equivariant functions *}
+
 lemma supp_fun_eqvt:
-  assumes a: "\<forall>p. p \<bullet> f = f"
+  assumes a: "\<And>p. p \<bullet> f = f"
   shows "supp f = {}"
   unfolding supp_def 
   using a by simp
 
-
 lemma fresh_fun_eqvt_app:
-  assumes a: "\<forall>p. p \<bullet> f = f"
+  assumes a: "\<And>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
   from a have "supp f = {}" by (simp add: supp_fun_eqvt)
   then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
     unfolding fresh_def
-    using supp_fun_app 
-    by auto
+    using supp_fun_app by auto
 qed