130 theorem progress:

   130 theorem progress:

   131   assumes a: "[] \<turnstile> t : T"

   131   assumes a: "[] \<turnstile> t : T"

   132   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

   132   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

   133 using a

   133 using a

   134 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

   134 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

   136 

   136 

   137 text {*

   137 text {*

   138   Done! Congratulations!

   138   Done! Congratulations!

   139 *}

   139 *}

   140 

   140