191 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);

   192  \<And>xs n x t. P xs (Var n) (Lam [x]. t);

   193  \<And>xs l r n. P xs (App l r) (Var n);

   194  (\<And>xs l1 r1 l2 r2. P xs l1 l2 \<Longrightarrow> P xs r1 r2 \<Longrightarrow> P xs (App l1 r1) (App l2 r2));

   195  \<And>xs l r x t. P xs (App l r) (Lam [x]. t);

   196  \<And>xs x t n. P xs (Lam [x]. t) (Var n);

   197  \<And>xs x t l1 r1. P xs (Lam [x]. t) (App l1 r1);

   198  \<And>x xs y s t.

   199     atom x \<sharp> (xs, Lam [y]. s) \<and>

   200     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>

   201 \<Longrightarrow> P (a :: (name \<times> name) list) b c"

   202   apply (induction_schema)

   203   apply (rule_tac y="b" and c="(a, c)" in lam.strong_exhaust)

   204   apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)

   205   apply simp_all[3] apply (metis)

   206   apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)

   207   apply simp_all[3] apply (metis, metis, metis)

   208   apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)

   209   apply simp_all[3] apply (metis)

   210   apply (simp add: fresh_star_def)

   211   apply metis

   212   apply lexicographic_order

   213   done

   214