[STATEMENT]
lemma Bex_image [reversal_rule]: assumes "(g \<circ> f) ` A = A" shows "Bex (f ` A) (P \<circ> g) = Bex A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bex (f ` A) (P \<circ> g) = Bex A P
[PROOF STEP]
unfolding Bex_image_comp[symmetric] image_comp \<open>(g \<circ> f) ` A = A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bex A P = Bex A P
[PROOF STEP]
..
                      
  \<comment> \<open>\<^const>\<open>insert\<close>\<close>