equal
deleted
inserted
replaced
110 by (perm_simp add: permute_minus_cancel) (rule refl) |
110 by (perm_simp add: permute_minus_cancel) (rule refl) |
111 |
111 |
112 lemma ex_eqvt2: |
112 lemma ex_eqvt2: |
113 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
113 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
114 by (perm_simp add: permute_minus_cancel) (rule refl) |
114 by (perm_simp add: permute_minus_cancel) (rule refl) |
115 |
|
116 lemma ex1_eqvt[eqvt]: |
|
117 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
|
118 unfolding Ex1_def |
|
119 by (perm_simp) (rule refl) |
|
120 |
115 |
121 lemma ex1_eqvt2: |
116 lemma ex1_eqvt2: |
122 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
117 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
123 by (perm_simp add: permute_minus_cancel) (rule refl) |
118 by (perm_simp add: permute_minus_cancel) (rule refl) |
124 |
119 |