106 lemma fresh_star_atom:

   107   "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s"

   108   apply (induct s)

   109   apply (simp add: fresh_set_empty)

   110   apply simp

   111   apply (unfold fresh_def)

   112   apply (simp add: supp_atom_insert)

   113   apply (rule conjI)

   114   apply (unfold fresh_star_def)

   115   apply simp

   116   apply (unfold fresh_def)

   117   apply (simp add: supp_at_base supp_atom)

   118   apply clarify

   119   apply auto

   120   done