DEFINITION clt_thead()
TYPE =
       k:K.u:T.c:C.(clt c (CTail k u c))
BODY =
        assume kK
        assume uT
        assume cC
          we proceed by induction on c to prove clt c (CTail k u c)
             case CSort : n:nat 
                the thesis becomes clt (CSort n) (CTail k u (CSort n))
                   by (clt_head . . .)
                   we proved clt (CSort n) (CHead (CSort n) k u)
clt (CSort n) (CTail k u (CSort n))
             case CHead : c0:C k0:K t:T 
                the thesis becomes clt (CHead c0 k0 t) (CTail k u (CHead c0 k0 t))
                (H) by induction hypothesis we know clt c0 (CTail k u c0)
                   by (clt_cong . . H . .)
                   we proved clt (CHead c0 k0 t) (CHead (CTail k u c0) k0 t)
clt (CHead c0 k0 t) (CTail k u (CHead c0 k0 t))
          we proved clt c (CTail k u c)
       we proved k:K.u:T.c:C.(clt c (CTail k u c))