diff -r e5fa8de0e4bd -r 4aa72a88b2c1 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 02:30:00 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 05:06:25 2011 +0000
@@ -124,6 +124,18 @@
 
 lemma the_eqvt:
   assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+  apply(rule the1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule theI'[OF unique])
+  done
+
+lemma the_eqvt2:
+  assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
   apply(simp add: ex1_eqvt2[symmetric])