- \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
-\def (cweight c) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
-t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (plus TMP_1
-TMP_4) in (let TMP_6 \def (S TMP_5) in (let TMP_12 \def (\lambda (n:
-nat).(let TMP_7 \def (cweight c) in (let TMP_8 \def (tweight u) in (let TMP_9
-\def (plus TMP_7 TMP_8) in (let TMP_10 \def (tweight t) in (let TMP_11 \def
-(plus TMP_9 TMP_10) in (lt TMP_11 n))))))) in (let TMP_13 \def (cweight c) in
-(let TMP_14 \def (tweight u) in (let TMP_15 \def (plus TMP_13 TMP_14) in (let
-TMP_16 \def (tweight t) in (let TMP_17 \def (plus TMP_15 TMP_16) in (let
-TMP_24 \def (\lambda (n: nat).(let TMP_18 \def (cweight c) in (let TMP_19
-\def (tweight u) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
-(tweight t) in (let TMP_22 \def (plus TMP_20 TMP_21) in (let TMP_23 \def (S
-n) in (lt TMP_22 TMP_23)))))))) in (let TMP_25 \def (cweight c) in (let
-TMP_26 \def (tweight u) in (let TMP_27 \def (plus TMP_25 TMP_26) in (let
-TMP_28 \def (tweight t) in (let TMP_29 \def (plus TMP_27 TMP_28) in (let
-TMP_30 \def (S TMP_29) in (let TMP_31 \def (le_n TMP_30) in (let TMP_32 \def
-(cweight c) in (let TMP_33 \def (tweight u) in (let TMP_34 \def (tweight t)
-in (let TMP_35 \def (plus TMP_33 TMP_34) in (let TMP_36 \def (plus TMP_32
-TMP_35) in (let TMP_37 \def (cweight c) in (let TMP_38 \def (tweight u) in
-(let TMP_39 \def (tweight t) in (let TMP_40 \def (plus_assoc_l TMP_37 TMP_38
-TMP_39) in (let TMP_41 \def (eq_ind_r nat TMP_17 TMP_24 TMP_31 TMP_36 TMP_40)
-in (let TMP_42 \def (cweight c) in (let TMP_43 \def (tweight u) in (let
-TMP_44 \def (tweight t) in (let TMP_45 \def (plus TMP_43 TMP_44) in (let
-TMP_46 \def (S TMP_45) in (let TMP_47 \def (plus TMP_42 TMP_46) in (let
-TMP_48 \def (cweight c) in (let TMP_49 \def (tweight u) in (let TMP_50 \def
-(tweight t) in (let TMP_51 \def (plus TMP_49 TMP_50) in (let TMP_52 \def
-(plus_n_Sm TMP_48 TMP_51) in (eq_ind nat TMP_6 TMP_12 TMP_41 TMP_47
-TMP_52))))))))))))))))))))))))))))))))))))))))))))).
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(eq_ind nat
+(S (plus (cweight c) (plus (tweight u) (tweight t)))) (\lambda (n: nat).(lt
+(plus (plus (cweight c) (tweight u)) (tweight t)) n)) (eq_ind_r nat (plus
+(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
+t))) (plus_assoc_l (cweight c) (tweight u) (tweight t))) (plus (cweight c) (S
+(plus (tweight u) (tweight t)))) (plus_n_Sm (cweight c) (plus (tweight u)
+(tweight t))))))).