399 

   400 lemma 

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

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

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

   404 apply(subst abs_eq_iff)

   405 apply(subst alphas_abs)

   406 apply(subst alphas)

   407 apply(rule impI)

   408 apply(erule exE)

   409 apply(simp add: supp_Pair)

   410 apply(simp add: Un_Diff)

   411 apply(simp add: fresh_star_union)

   412 apply(erule conjE)+

   413 apply(rule conjI)

   414 apply(rule trans)

   415 apply(rule sym)

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

   417 apply(simp add: supp_abs)

   418 apply(simp)

   419 apply(rule trans)

   420 apply(rule sym)

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

   422 apply(simp add: supp_abs)

   423 apply(simp)

   424 done

   425 

   426 

   427 

   428 (* support of concrete atom sets *)

   429 

   430 lemma 

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

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

   433   assumes asm: "finite as"

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

   435 apply(subst abs_eq_iff)

   436 apply(subst abs_eq_iff)

   437 apply(subst alphas_abs)

   438 apply(subst alphas_abs)

   439 apply(subst alphas)

   440 apply(subst alphas)

   441 apply(rule impI)

   442 apply(erule exE | erule conjE)+

   443 apply(simp add: abs_eq_iff)

   444 apply(simp add: alphas_abs)

   445 apply(simp add: alphas)

   446 apply(rule conjI)

   447 apply(simp add: supp_Pair Un_Diff)

   448 oops

   449 

   450