- \lambda (t: T).(match t in T return (\lambda (t0: T).(lt O (tweight t0)))
-with [(TSort _) \Rightarrow (le_n (S O)) | (TLRef _) \Rightarrow (le_n (S O))
-| (THead _ t0 t1) \Rightarrow (le_S_n (S O) (S (plus (tweight t0) (tweight
-t1))) (le_n_S (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S O (plus
-(tweight t0) (tweight t1)) (le_O_n (plus (tweight t0) (tweight t1))))))]).
+ \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).