+theorem tweight_lt:
+ \forall (t: T).(lt O (tweight t))
+\def
+ \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))))))]).
+