DEFINITION CTail()
TYPE =
       K→T→C→C
BODY =
FIXCTail{
         CTail:K→T→C→C
         :=λk:K
           .λt:T
             .λc:C
               .<λc1:C.C>
                 CASE c OF
                   CSort n⇒CHead (CSort n) k t
                 | CHead d h u⇒CHead (CTail k t d) h u
         }