\forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u))))
\def
\lambda (_: K).(\lambda (c: C).(\lambda (u: T).(eq_ind_r nat (plus (cweight
c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) (lt_reg_l O
(tweight u) (cweight c) (tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).
\forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u))))
\def
\lambda (_: K).(\lambda (c: C).(\lambda (u: T).(eq_ind_r nat (plus (cweight
c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) (lt_reg_l O
(tweight u) (cweight c) (tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).