873   by (perm_simp) (rule refl)

   873   by (perm_simp) (rule refl)

   874 

   874 

   875 lemma if_eqvt [eqvt]:

   875 lemma if_eqvt [eqvt]:

   876   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"

   876   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"

   877   by (simp add: permute_fun_def permute_bool_def)

   877   by (simp add: permute_fun_def permute_bool_def)

   878 

   882 

   879 lemma True_eqvt [eqvt]:

   883 lemma True_eqvt [eqvt]:

   880   shows "p \<bullet> True = True"

   884   shows "p \<bullet> True = True"

   881   unfolding permute_bool_def ..

   885   unfolding permute_bool_def ..

   882 

   886