src/CTT/CTT.thy

 lemma subst_prodE:
   assumes "p: Prod(A,B)"
     and "a: A"
     and "!!z. z: B(a) ==> c(z): C(z)"
   shows "c(p`a): C(p`a)"
-apply (rule prems ProdE)+
+apply (rule assms ProdE)+
 done
 
 
 subsection {* Tactics for type checking *}