200 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');

   201  \<And>A A' K x x' K'.

   202     \<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>

   203     \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K');

   204  \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);

   205  \<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');

   206  \<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');

   207  \<And>A A' B x x' B'.

   208     \<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>

   209     \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B');

   210  \<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));

   211  \<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');

   212  \<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');

   213  \<And>A A' M x x' M' B'.

   214     \<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>

   215     \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk>

   216 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>

   217    ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"

   218 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})

   219 apply(atomize (full))

   220 apply(rule my_equiv_res_forallR)

   221 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

   222 apply(rule my_equiv_res_forallR)

   223 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   224 apply(rule my_equiv_res_forallR)

   225 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   226 apply(rule my_equiv_res_forallR)

   227 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   228 apply(rule my_equiv_res_forallR)

   229 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   230 apply(rule my_equiv_res_forallR)

   231 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   232 apply(rule my_equiv_res_forallR)

   233 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   234 apply(rule my_equiv_res_forallR)

   235 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})

   236 apply(rule my_equiv_res_forallR)

   237 apply(tactic {*  (resolve_tac (Inductive.get_monos @{context})) 1 *})

   238 apply(rule Set.imp_mono)

   239 apply(rule impI)

   240 apply(assumption)

   241 apply(rule Set.imp_mono)

   242 

   243 

   244