(plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus
(cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight
c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight
(plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus
(cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight
c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight