--- a/LFex.thy	Thu Nov 26 10:32:31 2009 +0100
+++ b/LFex.thy	Thu Nov 26 10:52:24 2009 +0100
@@ -197,6 +197,51 @@
 
 thm akind_aty_atrm.induct
 
+lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
+ \<And>A A' K x x' K'.
+    \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk>
+    \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B');
+ \<And>A A' B x x' B'.
+    \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk>
+    \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B');
+ \<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j)); \<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y));
+ \<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M');
+ \<And>A A' M x x' M' B'.
+    \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk>
+    \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk>
+\<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
+   ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
+apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+apply(atomize (full))
+apply(rule my_equiv_res_forallR)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {*  (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule Set.imp_mono)
+apply(rule impI)
+apply(assumption)
+apply(rule Set.imp_mono)
+
+
+
 ML {*
 val rty_qty_rel =
   [(@{typ kind}, (@{typ KIND}, @{term akind})),