- \lambda (t: T).(let TMP_2 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
-in (lt O TMP_1))) in (let TMP_4 \def (\lambda (_: nat).(let TMP_3 \def (S O)
-in (le_n TMP_3))) in (let TMP_6 \def (\lambda (_: nat).(let TMP_5 \def (S O)
-in (le_n TMP_5))) in (let TMP_15 \def (\lambda (_: K).(\lambda (t0:
-T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
-(tweight t1))).(let TMP_7 \def (S O) in (let TMP_8 \def (tweight t0) in (let
-TMP_9 \def (tweight t1) in (let TMP_10 \def (plus TMP_8 TMP_9) in (let TMP_11
-\def (S O) in (let TMP_12 \def (tweight t0) in (let TMP_13 \def (tweight t1)
-in (let TMP_14 \def (le_plus_trans TMP_11 TMP_12 TMP_13 H) in (le_S TMP_7
-TMP_10 TMP_14)))))))))))))) in (T_ind TMP_2 TMP_4 TMP_6 TMP_15 t))))).
+ \lambda (t: T).(T_ind (\lambda (t0: T).(lt O (tweight t0))) (\lambda (_:
+nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda
+(t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
+(tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S
+O) (tweight t0) (tweight t1) H))))))) t).