70   apply (rule fset_finite_supp)

    70   apply (rule fset_finite_supp)

    71   done

    71   done

    72 

    72 

    73 lemma atom_map_fset_cong:

    73 lemma atom_map_fset_cong:

    74   shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"

    74   shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"

    76   apply(simp add: inj_on_def)

    76   apply(simp add: inj_on_def)

    77   done

    77   done

    78 

    78 

    79 lemma supp_map_fset_atom:

    79 lemma supp_map_fset_atom:

    80   shows "supp (map_fset atom S) = supp S"

    80   shows "supp (map_fset atom S) = supp S"