--- a/Nominal/Abs.thy	Thu Apr 15 12:07:54 2010 +0200
+++ b/Nominal/Abs.thy	Thu Apr 15 15:56:21 2010 +0200
@@ -397,6 +397,58 @@
 
 section {* BELOW is stuff that may or may not be needed *}
 
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
+  shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2)"
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE)
+apply(simp add: supp_Pair)
+apply(simp add: Un_Diff)
+apply(simp add: fresh_star_union)
+apply(erule conjE)+
+apply(rule conjI)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+done
+
+
+
+(* support of concrete atom sets *)
+
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
+  assumes asm: "finite as"
+  shows "(Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2) \<longrightarrow> Abs as (t1, t2) = Abs as (s1, s2)"
+apply(subst abs_eq_iff)
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE | erule conjE)+
+apply(simp add: abs_eq_iff)
+apply(simp add: alphas_abs)
+apply(simp add: alphas)
+apply(rule conjI)
+apply(simp add: supp_Pair Un_Diff)
+oops
+
+
+
 (* support of concrete atom sets *)
 
 lemma supp_atom_image: