1587   and     b: "finite (supp c)"

  1587   and     b: "finite (supp c)"

  1588   obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

  1588   obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

  1589   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]

  1589   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]

  1590   unfolding fresh_star_def fresh_def by blast

  1590   unfolding fresh_star_def fresh_def by blast

  1591 

  1591 

  1592 lemma at_set_avoiding2:

  1601 lemma at_set_avoiding2:

  1593   assumes "finite xs"

  1602   assumes "finite xs"

  1594   and     "finite (supp c)" "finite (supp x)"

  1603   and     "finite (supp c)" "finite (supp x)"

  1595   and     "xs \<sharp>* x"

  1604   and     "xs \<sharp>* x"

  1596   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"

  1605   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"