DEFINITION app1()
TYPE =
       C→T→T
BODY =
FIXapp1{
         app1:C→T→T
         :=λc:C.λt:T.<λc1:C.T> CASE c OF CSort ⇒t | CHead c0 k u⇒app1 c0 (THead k u t)
         }