(tweight u) in (let TMP_2 \def (tweight t0) in (let TMP_3 \def (plus TMP_1
TMP_2) in (S TMP_3))))].
+definition tle:
+ T \to (T \to Prop)
+\def
+ \lambda (t1: T).(\lambda (t2: T).(let TMP_1 \def (tweight t1) in (let TMP_2
+\def (tweight t2) in (le TMP_1 TMP_2)))).
+