793   by (perm_simp) (rule refl)

   793   by (perm_simp) (rule refl)

   794 

   794 

   795 lemma if_eqvt [eqvt]:

   795 lemma if_eqvt [eqvt]:

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

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

   797   by (simp add: permute_fun_def permute_bool_def)

   797   by (simp add: permute_fun_def permute_bool_def)

   798 

   802 

   799 lemma True_eqvt [eqvt]:

   803 lemma True_eqvt [eqvt]:

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

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

   801   unfolding permute_bool_def ..

   805   unfolding permute_bool_def ..

   802 

   806