src/HOL/Library/Countable_Set_Type.thy

 lift_definition cBex :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
 lift_definition cUNION :: "'a cset \<Rightarrow> ('a \<Rightarrow> 'b cset) \<Rightarrow> 'b cset"
   is "UNION" parametric UNION_transfer by simp
 definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
 
-lemma Union_conv_UNION: "\<Union>A = UNION A id"
+lemma Union_conv_UNION: "\<Union>A = \<Union>(id ` A)"
 by auto
 
 lemma cUnion_transfer [transfer_rule]:
   "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
 proof -
-  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
+  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. \<Union>(id ` A)) (\<lambda>A. cUNION A id)"
     by transfer_prover
   then show ?thesis by (simp flip: cUnion_def)
 qed
 
 lemmas cset_eqI = set_eqI[Transfer.transferred]