53 lemma at_set_avoiding5:

    54   assumes "finite xs"

    55   and     "finite (supp c)"

    56   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"

    57 using assms

    58 apply(erule_tac c="c" in at_set_avoiding)

    59 apply(auto)

    60 done

    61 

    62 lemma

    63   fixes c::"'a::fs"

    64   assumes a:  "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"

    65   shows "y = LetRec lrbs exp \<Longrightarrow> P"

    66 apply -

    67 apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))")

    68 apply(erule exE)

    69 apply(simp add: fresh_star_Pair)

    70 apply(erule conjE)+

    71 apply(simp add: multi_recs.fv_bn_eqvt)

    72 using Abs_rename_set'

    73 apply -

    74 apply(drule_tac x="p" in meta_spec)

    75 apply(drule_tac x="bs lrbs" in meta_spec)

    76 apply(drule_tac x="(lrbs, exp)" in meta_spec)

    77 apply(drule meta_mp)

    78 apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)

    79 apply(drule meta_mp)

    80 apply(simp add: multi_recs.bn_finite)

    81 apply(erule exE)

    82 apply(erule conjE)

    83 apply(rotate_tac 6)

    84 apply(drule sym)

    85 apply(simp add: multi_recs.fv_bn_eqvt)

    86 apply(rule a)

    87 apply(assumption)

    88 apply(clarify)

    89 apply(simp (no_asm) only: multi_recs.eq_iff)

    90 apply(rule at_set_avoiding1)

    91 apply(simp add: multi_recs.bn_finite)

    92 apply(simp add: supp_Pair finite_supp)

    93 apply(rule finite_sets_supp)

    94 apply(simp add: multi_recs.bn_finite)

    95 done