--- a/Nominal/Abs.thy	Sat Sep 25 08:38:04 2010 -0400
+++ b/Nominal/Abs.thy	Mon Sep 27 04:10:36 2010 -0400
@@ -570,6 +570,16 @@
   unfolding prod_fv.simps
   by (perm_simp) (rule refl)
 
+lemma prod_fv_supp:
+  shows "prod_fv supp supp = supp"
+by (rule ext)
+   (auto simp add: prod_fv.simps supp_Pair)
+
+lemma prod_alpha_eq:
+  shows "prod_alpha (op=) (op=) = (op=)"
+unfolding prod_alpha_def
+by (auto intro!: ext)
+
 
 end