DEFINITION getl_ctail_clen()
TYPE =
       ∀b:B
         .∀t:T
           .∀c:C
             .ex
               nat
               λn:nat
                 .getl
                   clen c
                   CTail (Bind b) t c
                   CHead (CSort n) (Bind b) t
BODY =
Show proof