- \lambda (k: K).(let TMP_6 \def (\lambda (k0: K).(\forall (u: T).(\forall (t:
-T).(let TMP_1 \def (\lambda (_: nat).O) in (let TMP_2 \def (weight_map TMP_1
-t) in (let TMP_3 \def (\lambda (_: nat).O) in (let TMP_4 \def (THead k0 u t)
-in (let TMP_5 \def (weight_map TMP_3 TMP_4) in (lt TMP_2 TMP_5))))))))) in
-(let TMP_161 \def (\lambda (b: B).(let TMP_31 \def (\lambda (b0: B).(\forall
-(u: T).(\forall (t: T).(let TMP_7 \def (\lambda (_: nat).O) in (let TMP_8
-\def (weight_map TMP_7 t) in (let TMP_30 \def (match b0 with [Abbr
-\Rightarrow (let TMP_21 \def (\lambda (_: nat).O) in (let TMP_22 \def
-(weight_map TMP_21 u) in (let TMP_23 \def (\lambda (_: nat).O) in (let TMP_24
-\def (\lambda (_: nat).O) in (let TMP_25 \def (weight_map TMP_24 u) in (let
-TMP_26 \def (S TMP_25) in (let TMP_27 \def (wadd TMP_23 TMP_26) in (let
-TMP_28 \def (weight_map TMP_27 t) in (let TMP_29 \def (plus TMP_22 TMP_28) in
-(S TMP_29)))))))))) | Abst \Rightarrow (let TMP_15 \def (\lambda (_: nat).O)
-in (let TMP_16 \def (weight_map TMP_15 u) in (let TMP_17 \def (\lambda (_:
-nat).O) in (let TMP_18 \def (wadd TMP_17 O) in (let TMP_19 \def (weight_map
-TMP_18 t) in (let TMP_20 \def (plus TMP_16 TMP_19) in (S TMP_20))))))) | Void
-\Rightarrow (let TMP_9 \def (\lambda (_: nat).O) in (let TMP_10 \def
-(weight_map TMP_9 u) in (let TMP_11 \def (\lambda (_: nat).O) in (let TMP_12
-\def (wadd TMP_11 O) in (let TMP_13 \def (weight_map TMP_12 t) in (let TMP_14
-\def (plus TMP_10 TMP_13) in (S TMP_14)))))))]) in (lt TMP_8 TMP_30))))))) in
-(let TMP_106 \def (\lambda (u: T).(\lambda (t: T).(let TMP_32 \def (\lambda
-(_: nat).O) in (let TMP_33 \def (weight_map TMP_32 t) in (let TMP_34 \def
-(\lambda (_: nat).O) in (let TMP_35 \def (weight_map TMP_34 t) in (let TMP_36
-\def (S TMP_35) in (let TMP_37 \def (\lambda (_: nat).O) in (let TMP_38 \def
-(weight_map TMP_37 u) in (let TMP_39 \def (\lambda (_: nat).O) in (let TMP_40
-\def (\lambda (_: nat).O) in (let TMP_41 \def (weight_map TMP_40 u) in (let
-TMP_42 \def (S TMP_41) in (let TMP_43 \def (wadd TMP_39 TMP_42) in (let
-TMP_44 \def (weight_map TMP_43 t) in (let TMP_45 \def (plus TMP_38 TMP_44) in
-(let TMP_46 \def (S TMP_45) in (let TMP_47 \def (\lambda (_: nat).O) in (let
-TMP_48 \def (weight_map TMP_47 t) in (let TMP_49 \def (lt_n_Sn TMP_48) in
-(let TMP_50 \def (\lambda (_: nat).O) in (let TMP_51 \def (weight_map TMP_50
-t) in (let TMP_52 \def (\lambda (_: nat).O) in (let TMP_53 \def (weight_map
-TMP_52 u) in (let TMP_54 \def (\lambda (_: nat).O) in (let TMP_55 \def
-(\lambda (_: nat).O) in (let TMP_56 \def (weight_map TMP_55 u) in (let TMP_57
-\def (S TMP_56) in (let TMP_58 \def (wadd TMP_54 TMP_57) in (let TMP_59 \def
-(weight_map TMP_58 t) in (let TMP_60 \def (plus TMP_53 TMP_59) in (let TMP_61
-\def (\lambda (_: nat).O) in (let TMP_62 \def (weight_map TMP_61 t) in (let
-TMP_63 \def (\lambda (_: nat).O) in (let TMP_64 \def (\lambda (_: nat).O) in
-(let TMP_65 \def (weight_map TMP_64 u) in (let TMP_66 \def (S TMP_65) in (let
-TMP_67 \def (wadd TMP_63 TMP_66) in (let TMP_68 \def (weight_map TMP_67 t) in
-(let TMP_69 \def (\lambda (_: nat).O) in (let TMP_70 \def (weight_map TMP_69
-u) in (let TMP_71 \def (\lambda (_: nat).O) in (let TMP_72 \def (\lambda (_:
-nat).O) in (let TMP_73 \def (weight_map TMP_72 u) in (let TMP_74 \def (S
-TMP_73) in (let TMP_75 \def (wadd TMP_71 TMP_74) in (let TMP_76 \def
-(weight_map TMP_75 t) in (let TMP_77 \def (plus TMP_70 TMP_76) in (let TMP_78
-\def (\lambda (_: nat).O) in (let TMP_79 \def (wadd TMP_78 O) in (let TMP_80
-\def (weight_map TMP_79 t) in (let TMP_87 \def (\lambda (n: nat).(let TMP_81
-\def (\lambda (_: nat).O) in (let TMP_82 \def (\lambda (_: nat).O) in (let
-TMP_83 \def (weight_map TMP_82 u) in (let TMP_84 \def (S TMP_83) in (let
-TMP_85 \def (wadd TMP_81 TMP_84) in (let TMP_86 \def (weight_map TMP_85 t) in
-(le n TMP_86)))))))) in (let TMP_88 \def (\lambda (_: nat).O) in (let TMP_89
-\def (weight_map TMP_88 u) in (let TMP_90 \def (weight_add_S t TMP_89) in
-(let TMP_91 \def (\lambda (_: nat).O) in (let TMP_92 \def (weight_map TMP_91
-t) in (let TMP_93 \def (weight_add_O t) in (let TMP_94 \def (eq_ind nat
-TMP_80 TMP_87 TMP_90 TMP_92 TMP_93) in (let TMP_95 \def (\lambda (_: nat).O)
-in (let TMP_96 \def (weight_map TMP_95 u) in (let TMP_97 \def (\lambda (_:
-nat).O) in (let TMP_98 \def (\lambda (_: nat).O) in (let TMP_99 \def
-(weight_map TMP_98 u) in (let TMP_100 \def (S TMP_99) in (let TMP_101 \def
-(wadd TMP_97 TMP_100) in (let TMP_102 \def (weight_map TMP_101 t) in (let
-TMP_103 \def (le_plus_r TMP_96 TMP_102) in (let TMP_104 \def (le_trans TMP_62
-TMP_68 TMP_77 TMP_94 TMP_103) in (let TMP_105 \def (le_n_S TMP_51 TMP_60
-TMP_104) in (lt_le_trans TMP_33 TMP_36 TMP_46 TMP_49
-TMP_105)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
- in (let TMP_133 \def (\lambda (u: T).(\lambda (t: T).(let TMP_107 \def
-(\lambda (_: nat).O) in (let TMP_108 \def (weight_map TMP_107 t) in (let
-TMP_115 \def (\lambda (n: nat).(let TMP_109 \def (\lambda (_: nat).O) in (let
-TMP_110 \def (weight_map TMP_109 t) in (let TMP_111 \def (\lambda (_: nat).O)
-in (let TMP_112 \def (weight_map TMP_111 u) in (let TMP_113 \def (plus
-TMP_112 n) in (let TMP_114 \def (S TMP_113) in (lt TMP_110 TMP_114)))))))) in
-(let TMP_116 \def (\lambda (_: nat).O) in (let TMP_117 \def (weight_map
-TMP_116 t) in (let TMP_118 \def (\lambda (_: nat).O) in (let TMP_119 \def
-(weight_map TMP_118 u) in (let TMP_120 \def (\lambda (_: nat).O) in (let
-TMP_121 \def (weight_map TMP_120 t) in (let TMP_122 \def (plus TMP_119
-TMP_121) in (let TMP_123 \def (\lambda (_: nat).O) in (let TMP_124 \def
-(weight_map TMP_123 u) in (let TMP_125 \def (\lambda (_: nat).O) in (let
-TMP_126 \def (weight_map TMP_125 t) in (let TMP_127 \def (le_plus_r TMP_124
-TMP_126) in (let TMP_128 \def (le_n_S TMP_117 TMP_122 TMP_127) in (let
-TMP_129 \def (\lambda (_: nat).O) in (let TMP_130 \def (wadd TMP_129 O) in
-(let TMP_131 \def (weight_map TMP_130 t) in (let TMP_132 \def (weight_add_O
-t) in (eq_ind_r nat TMP_108 TMP_115 TMP_128 TMP_131
-TMP_132))))))))))))))))))))))) in (let TMP_160 \def (\lambda (u: T).(\lambda
-(t: T).(let TMP_134 \def (\lambda (_: nat).O) in (let TMP_135 \def
-(weight_map TMP_134 t) in (let TMP_142 \def (\lambda (n: nat).(let TMP_136
-\def (\lambda (_: nat).O) in (let TMP_137 \def (weight_map TMP_136 t) in (let
-TMP_138 \def (\lambda (_: nat).O) in (let TMP_139 \def (weight_map TMP_138 u)
-in (let TMP_140 \def (plus TMP_139 n) in (let TMP_141 \def (S TMP_140) in (lt
-TMP_137 TMP_141)))))))) in (let TMP_143 \def (\lambda (_: nat).O) in (let
-TMP_144 \def (weight_map TMP_143 t) in (let TMP_145 \def (\lambda (_: nat).O)
-in (let TMP_146 \def (weight_map TMP_145 u) in (let TMP_147 \def (\lambda (_:
-nat).O) in (let TMP_148 \def (weight_map TMP_147 t) in (let TMP_149 \def
-(plus TMP_146 TMP_148) in (let TMP_150 \def (\lambda (_: nat).O) in (let
-TMP_151 \def (weight_map TMP_150 u) in (let TMP_152 \def (\lambda (_: nat).O)
-in (let TMP_153 \def (weight_map TMP_152 t) in (let TMP_154 \def (le_plus_r
-TMP_151 TMP_153) in (let TMP_155 \def (le_n_S TMP_144 TMP_149 TMP_154) in
-(let TMP_156 \def (\lambda (_: nat).O) in (let TMP_157 \def (wadd TMP_156 O)
-in (let TMP_158 \def (weight_map TMP_157 t) in (let TMP_159 \def
-(weight_add_O t) in (eq_ind_r nat TMP_135 TMP_142 TMP_155 TMP_158
-TMP_159))))))))))))))))))))))) in (B_ind TMP_31 TMP_106 TMP_133 TMP_160
-b)))))) in (let TMP_174 \def (\lambda (_: F).(\lambda (u: T).(\lambda (t:
-T).(let TMP_162 \def (\lambda (_: nat).O) in (let TMP_163 \def (weight_map
-TMP_162 t) in (let TMP_164 \def (\lambda (_: nat).O) in (let TMP_165 \def
-(weight_map TMP_164 u) in (let TMP_166 \def (\lambda (_: nat).O) in (let
-TMP_167 \def (weight_map TMP_166 t) in (let TMP_168 \def (plus TMP_165
-TMP_167) in (let TMP_169 \def (\lambda (_: nat).O) in (let TMP_170 \def
-(weight_map TMP_169 u) in (let TMP_171 \def (\lambda (_: nat).O) in (let
-TMP_172 \def (weight_map TMP_171 t) in (let TMP_173 \def (le_plus_r TMP_170
-TMP_172) in (le_n_S TMP_163 TMP_168 TMP_173)))))))))))))))) in (K_ind TMP_6
-TMP_161 TMP_174 k)))).
-
-theorem tle_r:
- \forall (t: T).(tle t t)
-\def
- \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
-in (let TMP_2 \def (tweight t0) in (le TMP_1 TMP_2)))) in (let TMP_5 \def
-(\lambda (_: nat).(let TMP_4 \def (S O) in (le_n TMP_4))) in (let TMP_7 \def
-(\lambda (_: nat).(let TMP_6 \def (S O) in (le_n TMP_6))) in (let TMP_12 \def
-(\lambda (_: K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight
-t0))).(\lambda (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(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 TMP_10) in (le_n TMP_11))))))))))
-in (T_ind TMP_3 TMP_5 TMP_7 TMP_12 t))))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
+(weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
+k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
+(t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
+(u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
+(weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
+nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
+nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
+(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
+u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
+(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
+(weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
+(\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
+(_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
+(weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
+(weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
+(wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
+(\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
+nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
+(weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
+nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
+nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
+(\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
+(weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
+(\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
+nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
+(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
+nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
+(_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
+T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
+(le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
+nat).O) t)))))) k).