275   and     a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"

   275   and     a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"

   276   shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"

   276   shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"

   277 using a0 a1 a2 a3 a4 a5 a6 a7 a8

   277 using a0 a1 a2 a3 a4 a5 a6 a7 a8

   278 *)

   278 *)

   279 

   279 

   280 lemma "\<lbrakk>P TYP;

   281 lemma "\<lbrakk>P TYP;

   281   \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);

   282   \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);

   282   \<And>id. Q (TCONST id);

   283   \<And>id. Q (TCONST id);

   283   \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);

   284   \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);

   284   \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);

   285   \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);