DEFINITION clt_head()
TYPE =
       ∀k:K.∀c:C.∀u:T.(clt c (CHead c k u))
BODY =
        assume : K
        assume c: C
        assume u: T
          (h1) 
             (h1) 
                by (le_n .)
le (cweight c) (cweight c)
             end of h1
             (h2) 
                by (tweight_lt .)
lt O (tweight u)
             end of h2
             by (le_lt_plus_plus . . . . h1 h2)
lt (plus (cweight c) O) (plus (cweight c) (tweight u))
          end of h1
          (h2) 
             by (plus_n_O .)
eq nat (cweight c) (plus (cweight c) O)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved lt (cweight c) (plus (cweight c) (tweight u))
          that is equivalent to clt c (CHead c __3 u)
       we proved K→∀c:C.∀u:T.(clt c (CHead c __3 u))