DEFINITION clt_thead()
TYPE =
       ∀k:K.∀u:T.∀c:C.(clt c (CTail k u c))
BODY =
        assume k: K
        assume u: T
        assume c: C
          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))