--- a/Nominal-General/Nominal2_Supp.thy	Thu Sep 02 18:10:06 2010 +0800
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Sep 03 20:48:45 2010 +0800
@@ -543,5 +543,12 @@
   using fin
   by (simp add: supp_of_fin_sets)
 
+lemma supp_set:
+  fixes xs :: "('a::fs) list"
+  shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons finite_set supp_of_fin_insert)
+done
 
 end