-c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) (lt_le_S (plus
-(cweight c) O) (plus (cweight c) (tweight u)) (plus_le_lt_compat (cweight c)
-(cweight c) O (tweight u) (le_n (cweight c)) (tweight_lt u))) (cweight c)
-(plus_n_O (cweight c))))).
+c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u))))
+(plus_le_lt_compat (cweight c) (cweight c) O (tweight u) (le_n (cweight c))
+(tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).