--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 09:11:30 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 13:39:15 2012 +0200
@@ -268,9 +268,19 @@
   apply simp
   apply simp
   apply simp
-  (* The last subgoal would be obvious if we'd define it with a recusor
-     and have eqvt for the function *)
-  sorry
+  apply clarify
+  apply (rule_tac s="(x \<leftrightarrow> xa) \<bullet> swapequal_sumC ((hla \<leftrightarrow> x) \<bullet> la, (hra \<leftrightarrow> x) \<bullet> ra, ta)" in trans)
+  apply (simp only: permute_pure)
+  apply (simp add: eqvt_at_def fresh_Pair_elim)
+  apply (simp add: flip_fresh_fresh)
+  apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hla \<leftrightarrow> x) \<bullet> la = (hla \<leftrightarrow> xa) \<bullet> la")
+  apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hra \<leftrightarrow> x) \<bullet> ra = (hra \<leftrightarrow> xa) \<bullet> ra")
+  apply simp
+  apply (subst permute_eqvt)
+  apply (simp add: flip_fresh_fresh flip_eqvt)
+  apply (subst permute_eqvt)
+  apply (simp add: flip_fresh_fresh flip_eqvt)
+  done
 
 termination (eqvt) by lexicographic_order
 
@@ -341,7 +351,37 @@
 lemma swapequal_reorder: "
   a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow>
   swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)"
-  sorry
+  apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh)
+  apply (rule_tac x="(a, b, x, y, t, s, xs, aa)" and ?'a="name" in obtain_fresh)
+  apply (rename_tac f g)
+  apply (simp add: fresh_Pair_elim fresh_at_base)
+  apply (subst swapequal.simps)
+  apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1]
+  apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t")
+  prefer 2
+  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
+  apply (subst swapequal.simps)
+  apply (simp add: fresh_Pair fresh_Cons fresh_permute_left)
+  apply rule apply assumption
+  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
+  apply (subst swapequal.simps)
+  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
+  apply rule apply (rotate_tac 12)
+  apply assumption
+  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
+  apply (subst swapequal.simps)
+  apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left)
+  apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t")
+  prefer 2
+  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
+  apply rule apply assumption
+  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
+  apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
+  apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
+  apply simp
+  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
+  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
+  done
 
 lemma swapequal_lambda:
   assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs"