diff -r 9c0df9901acf -r b9a16d627bfd Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Sun Jun 19 13:10:15 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Sun Jun 19 13:14:37 2011 +0900
@@ -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