--- a/Nominal-General/Nominal2_Base.thy	Thu Jun 03 11:48:44 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Thu Jun 03 15:02:52 2010 +0200
@@ -385,6 +385,11 @@
   unfolding permute_perm_def
   by (auto simp add: swap_atom expand_perm_eq)
 
+lemma uminus_eqvt:
+  fixes p q::"perm"
+  shows "p \<bullet> (- q) = - (p \<bullet> q)"
+  unfolding permute_perm_def
+  by (simp add: diff_minus minus_add add_assoc)
 
 subsection {* Permutations for functions *}