--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 01:45:07 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 12:14:40 2010 +0800
@@ -41,7 +41,7 @@
 
 lemma test: 
   "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-oops
+sorry
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
@@ -49,7 +49,6 @@
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
 
-(*
 lemma supp_fv:
   "supp t = fv_trm t \<and> supp b = fv_bn b"
 apply(rule single_let.induct)
@@ -65,19 +64,17 @@
 apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)")
 apply(simp only: single_let.fv_defs)
 apply(simp only: supp_abs)
+apply(simp)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: single_let.perm_simps)
 apply(simp only: single_let.eq_iff)
+apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(simp only: Abs_eq_iff)
 apply(subst test)
-apply(simp only: Abs_eq_iff[symmetric])
-apply(simp only: alphas_abs[symmetric])
-apply(simp only: eqvts)
-thm Abs_eq_iff
-apply(simp only: alphas)
+apply(rule refl)
 sorry
-*)
+
 (*
-
 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"