--- a/Nominal/Nominal2_Base.thy	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Thu Jun 16 20:07:03 2011 +0100
@@ -1626,6 +1626,12 @@
 definition
   "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 
+lemma eqvt_boolI:
+  fixes f::"bool"
+  shows "eqvt f"
+unfolding eqvt_def by (simp add: permute_bool_def)
+
+
 text {* equivariance of a function at a given argument *}
 
 definition