--- a/Nominal/Ex/LamTest.thy	Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Mon Jan 10 11:36:55 2011 +0000
@@ -25,6 +25,14 @@
 apply(rule fin)
 done
 
+lemma finite_supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "finite (supp (f x))"
+apply(rule finite_subset)
+apply(rule supp_eqvt_at[OF asm fin])
+apply(rule fin)
+done
 
 definition
  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
@@ -1702,6 +1710,16 @@
 thm depth.psimps
 thm depth.simps
 
+
+lemma swap_set_not_in_at:
+  fixes a b::"'a::at"
+  and   S::"'a::at set"
+  assumes a: "a \<notin> S" "b \<notin> S"
+  shows "(a \<leftrightarrow> b) \<bullet> S = S"
+  unfolding permute_set_eq
+  using a by (auto simp add: permute_flip_at)
+
+
 nominal_primrec 
   frees :: "lam \<Rightarrow> name set"
 where
@@ -1724,6 +1742,7 @@
 apply(simp add: Abs_fresh_iff)
 apply(simp)
 apply(drule test)
+apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
 oops
 
 nominal_primrec