diff -r 319964ecf1f6 -r 4d01d1056e22 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Thu Mar 29 10:37:09 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Thu Mar 29 10:37:41 2012 +0200
@@ -188,6 +188,30 @@
   apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
   done
 
+lemma aux_induct:  "\<lbrakk>\<And>xs n m. P xs (Var n) (Var m); \<And>xs n l r. P xs (Var n) (App l r);
+ \<And>xs n x t. P xs (Var n) (Lam [x]. t);
+ \<And>xs l r n. P xs (App l r) (Var n);
+ (\<And>xs l1 r1 l2 r2. P xs l1 l2 \<Longrightarrow> P xs r1 r2 \<Longrightarrow> P xs (App l1 r1) (App l2 r2));
+ \<And>xs l r x t. P xs (App l r) (Lam [x]. t);
+ \<And>xs x t n. P xs (Lam [x]. t) (Var n);
+ \<And>xs x t l1 r1. P xs (Lam [x]. t) (App l1 r1);
+ \<And>x xs y s t.
+    atom x \<sharp> (xs, Lam [y]. s) \<and>
+    atom y \<sharp> (x, xs, Lam [x]. t) \<Longrightarrow> P ((x, y) # xs) t s \<Longrightarrow> P xs (Lam [x]. t) (Lam [y]. s)\<rbrakk>
+\<Longrightarrow> P (a :: (name \<times> name) list) b c"
+  apply (induction_schema)
+  apply (rule_tac y="b" and c="(a, c)" in lam.strong_exhaust)
+  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
+  apply simp_all[3] apply (metis)
+  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
+  apply simp_all[3] apply (metis, metis, metis)
+  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
+  apply simp_all[3] apply (metis)
+  apply (simp add: fresh_star_def)
+  apply metis
+  apply lexicographic_order
+  done
+
 end