426 

   426 lemma 

   427 

   427   fixes t1 s1::"'a::fs"

   428 (* support of concrete atom sets *)

   428   and   t2 s2::"'b::fs"

   429   shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"

   430 apply(subst abs_eq_iff)

   431 apply(subst alphas_abs)

   432 apply(subst alphas)

   433 apply(rule impI)

   434 apply(erule exE)

   435 apply(simp add: supp_Pair)

   436 apply(simp add: Un_Diff)

   437 apply(simp add: fresh_star_union)

   438 apply(erule conjE)+

   439 apply(rule conjI)

   440 apply(rule trans)

   441 apply(rule sym)

   442 apply(rule_tac p="p" in supp_perm_eq)

   443 apply(simp add: supp_abs)

   444 apply(simp)

   445 apply(rule trans)

   446 apply(rule sym)

   447 apply(rule_tac p="p" in supp_perm_eq)

   448 apply(simp add: supp_abs)

   449 apply(simp)

   450 done

   451 

   452 lemma fresh_star_eq:

   453   assumes a: "as \<sharp>* p"

   454   shows "\<forall>a \<in> as. p \<bullet> a = a"

   455 using a by (simp add: fresh_star_def fresh_def supp_perm)

   456 

   457 lemma fresh_star_set_eq:

   458   assumes a: "as \<sharp>* p"

   459   shows "p \<bullet> as = as"

   460 using a 

   461 apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)

   462 apply(auto)

   463 by (metis permute_atom_def)

   434   shows "(Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2) \<longrightarrow> Abs as (t1, t2) = Abs as (s1, s2)"

   469   shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"