1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/subst0/fwd.ma".
19 include "basic_1/lift/tlt.ma".
21 theorem subst0_weight_le:
22 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
23 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
24 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
25 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
27 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
28 (H: (subst0 d u t z)).(let TMP_3 \def (\lambda (n: nat).(\lambda (t0:
29 T).(\lambda (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall
30 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
31 (weight_map f (lift (S n) O t0)) (g n)) \to (let TMP_1 \def (weight_map f t2)
32 in (let TMP_2 \def (weight_map g t1) in (le TMP_1 TMP_2))))))))))) in (let
33 TMP_33 \def (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to
34 nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f
35 m) (g m))))).(\lambda (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(let
36 TMP_4 \def (S i) in (let TMP_5 \def (lift TMP_4 O v) in (let TMP_6 \def
37 (weight_map f TMP_5) in (let TMP_7 \def (TLRef i) in (let TMP_8 \def
38 (weight_map g TMP_7) in (let TMP_9 \def (S i) in (let TMP_10 \def (lift TMP_9
39 O v) in (let TMP_11 \def (weight_map f TMP_10) in (let TMP_12 \def (S TMP_11)
40 in (let TMP_13 \def (TLRef i) in (let TMP_14 \def (weight_map g TMP_13) in
41 (let TMP_15 \def (S TMP_14) in (let TMP_16 \def (S i) in (let TMP_17 \def
42 (lift TMP_16 O v) in (let TMP_18 \def (weight_map f TMP_17) in (let TMP_19
43 \def (S TMP_18) in (let TMP_20 \def (S TMP_19) in (let TMP_21 \def (TLRef i)
44 in (let TMP_22 \def (weight_map g TMP_21) in (let TMP_23 \def (S TMP_22) in
45 (let TMP_24 \def (S i) in (let TMP_25 \def (lift TMP_24 O v) in (let TMP_26
46 \def (weight_map f TMP_25) in (let TMP_27 \def (S TMP_26) in (let TMP_28 \def
47 (TLRef i) in (let TMP_29 \def (weight_map g TMP_28) in (let TMP_30 \def
48 (le_n_S TMP_27 TMP_29 H1) in (let TMP_31 \def (le_S TMP_20 TMP_23 TMP_30) in
49 (let TMP_32 \def (le_S_n TMP_12 TMP_15 TMP_31) in (le_S_n TMP_6 TMP_8
50 TMP_32)))))))))))))))))))))))))))))))))))) in (let TMP_146 \def (\lambda (v:
51 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
52 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
53 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
54 i) O v)) (g i)) \to (le (weight_map f u2) (weight_map g u1)))))))).(\lambda
55 (t0: T).(\lambda (k: K).(let TMP_38 \def (\lambda (k0: K).(\forall (f: ((nat
56 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g
57 m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (let TMP_34 \def
58 (THead k0 u2 t0) in (let TMP_35 \def (weight_map f TMP_34) in (let TMP_36
59 \def (THead k0 u1 t0) in (let TMP_37 \def (weight_map g TMP_36) in (le TMP_35
60 TMP_37)))))))))) in (let TMP_131 \def (\lambda (b: B).(let TMP_45 \def
61 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
62 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
63 i) O v)) (g i)) \to (let TMP_39 \def (Bind b0) in (let TMP_40 \def (THead
64 TMP_39 u2 t0) in (let TMP_41 \def (weight_map f TMP_40) in (let TMP_42 \def
65 (Bind b0) in (let TMP_43 \def (THead TMP_42 u1 t0) in (let TMP_44 \def
66 (weight_map g TMP_43) in (le TMP_41 TMP_44)))))))))))) in (let TMP_86 \def
67 (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2:
68 ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift
69 (S i) O v)) (g i))).(let TMP_46 \def (weight_map f u2) in (let TMP_47 \def
70 (weight_map f u2) in (let TMP_48 \def (S TMP_47) in (let TMP_49 \def (wadd f
71 TMP_48) in (let TMP_50 \def (weight_map TMP_49 t0) in (let TMP_51 \def (plus
72 TMP_46 TMP_50) in (let TMP_52 \def (weight_map g u1) in (let TMP_53 \def
73 (weight_map g u1) in (let TMP_54 \def (S TMP_53) in (let TMP_55 \def (wadd g
74 TMP_54) in (let TMP_56 \def (weight_map TMP_55 t0) in (let TMP_57 \def (plus
75 TMP_52 TMP_56) in (let TMP_58 \def (weight_map f u2) in (let TMP_59 \def
76 (weight_map g u1) in (let TMP_60 \def (weight_map f u2) in (let TMP_61 \def
77 (S TMP_60) in (let TMP_62 \def (wadd f TMP_61) in (let TMP_63 \def
78 (weight_map TMP_62 t0) in (let TMP_64 \def (weight_map g u1) in (let TMP_65
79 \def (S TMP_64) in (let TMP_66 \def (wadd g TMP_65) in (let TMP_67 \def
80 (weight_map TMP_66 t0) in (let TMP_68 \def (H1 f g H2 H3) in (let TMP_69 \def
81 (weight_map f u2) in (let TMP_70 \def (S TMP_69) in (let TMP_71 \def (wadd f
82 TMP_70) in (let TMP_72 \def (weight_map g u1) in (let TMP_73 \def (S TMP_72)
83 in (let TMP_74 \def (wadd g TMP_73) in (let TMP_83 \def (\lambda (n:
84 nat).(let TMP_75 \def (weight_map f u2) in (let TMP_76 \def (S TMP_75) in
85 (let TMP_77 \def (weight_map g u1) in (let TMP_78 \def (S TMP_77) in (let
86 TMP_79 \def (weight_map f u2) in (let TMP_80 \def (weight_map g u1) in (let
87 TMP_81 \def (H1 f g H2 H3) in (let TMP_82 \def (le_n_S TMP_79 TMP_80 TMP_81)
88 in (wadd_le f g H2 TMP_76 TMP_78 TMP_82 n)))))))))) in (let TMP_84 \def
89 (weight_le t0 TMP_71 TMP_74 TMP_83) in (let TMP_85 \def (le_plus_plus TMP_58
90 TMP_59 TMP_63 TMP_67 TMP_68 TMP_84) in (le_n_S TMP_51 TMP_57
91 TMP_85))))))))))))))))))))))))))))))))))))) in (let TMP_108 \def (\lambda (f:
92 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
93 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
94 i))).(let TMP_87 \def (weight_map f u2) in (let TMP_88 \def (wadd f O) in
95 (let TMP_89 \def (weight_map TMP_88 t0) in (let TMP_90 \def (plus TMP_87
96 TMP_89) in (let TMP_91 \def (weight_map g u1) in (let TMP_92 \def (wadd g O)
97 in (let TMP_93 \def (weight_map TMP_92 t0) in (let TMP_94 \def (plus TMP_91
98 TMP_93) in (let TMP_95 \def (weight_map f u2) in (let TMP_96 \def (weight_map
99 g u1) in (let TMP_97 \def (wadd f O) in (let TMP_98 \def (weight_map TMP_97
100 t0) in (let TMP_99 \def (wadd g O) in (let TMP_100 \def (weight_map TMP_99
101 t0) in (let TMP_101 \def (H1 f g H2 H3) in (let TMP_102 \def (wadd f O) in
102 (let TMP_103 \def (wadd g O) in (let TMP_105 \def (\lambda (n: nat).(let
103 TMP_104 \def (le_O_n O) in (wadd_le f g H2 O O TMP_104 n))) in (let TMP_106
104 \def (weight_le t0 TMP_102 TMP_103 TMP_105) in (let TMP_107 \def
105 (le_plus_plus TMP_95 TMP_96 TMP_98 TMP_100 TMP_101 TMP_106) in (le_n_S TMP_90
106 TMP_94 TMP_107))))))))))))))))))))))))) in (let TMP_130 \def (\lambda (f:
107 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
108 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
109 i))).(let TMP_109 \def (weight_map f u2) in (let TMP_110 \def (wadd f O) in
110 (let TMP_111 \def (weight_map TMP_110 t0) in (let TMP_112 \def (plus TMP_109
111 TMP_111) in (let TMP_113 \def (weight_map g u1) in (let TMP_114 \def (wadd g
112 O) in (let TMP_115 \def (weight_map TMP_114 t0) in (let TMP_116 \def (plus
113 TMP_113 TMP_115) in (let TMP_117 \def (weight_map f u2) in (let TMP_118 \def
114 (weight_map g u1) in (let TMP_119 \def (wadd f O) in (let TMP_120 \def
115 (weight_map TMP_119 t0) in (let TMP_121 \def (wadd g O) in (let TMP_122 \def
116 (weight_map TMP_121 t0) in (let TMP_123 \def (H1 f g H2 H3) in (let TMP_124
117 \def (wadd f O) in (let TMP_125 \def (wadd g O) in (let TMP_127 \def (\lambda
118 (n: nat).(let TMP_126 \def (le_O_n O) in (wadd_le f g H2 O O TMP_126 n))) in
119 (let TMP_128 \def (weight_le t0 TMP_124 TMP_125 TMP_127) in (let TMP_129 \def
120 (le_plus_plus TMP_117 TMP_118 TMP_120 TMP_122 TMP_123 TMP_128) in (le_n_S
121 TMP_112 TMP_116 TMP_129))))))))))))))))))))))))) in (B_ind TMP_45 TMP_86
122 TMP_108 TMP_130 b)))))) in (let TMP_145 \def (\lambda (_: F).(\lambda (f0:
123 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
124 nat).(le (f0 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v))
125 (g i))).(let TMP_132 \def (weight_map f0 u2) in (let TMP_133 \def (weight_map
126 f0 t0) in (let TMP_134 \def (plus TMP_132 TMP_133) in (let TMP_135 \def
127 (weight_map g u1) in (let TMP_136 \def (weight_map g t0) in (let TMP_137 \def
128 (plus TMP_135 TMP_136) in (let TMP_138 \def (weight_map f0 u2) in (let
129 TMP_139 \def (weight_map g u1) in (let TMP_140 \def (weight_map f0 t0) in
130 (let TMP_141 \def (weight_map g t0) in (let TMP_142 \def (H1 f0 g H2 H3) in
131 (let TMP_143 \def (weight_le t0 f0 g H2) in (let TMP_144 \def (le_plus_plus
132 TMP_138 TMP_139 TMP_140 TMP_141 TMP_142 TMP_143) in (le_n_S TMP_134 TMP_137
133 TMP_144))))))))))))))))))) in (K_ind TMP_38 TMP_131 TMP_145 k)))))))))))) in
134 (let TMP_302 \def (\lambda (k: K).(let TMP_151 \def (\lambda (k0: K).(\forall
135 (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i)
136 v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
137 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
138 (s k0 i)) O v)) (g (s k0 i))) \to (le (weight_map f t2) (weight_map g
139 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
140 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
141 f (lift (S i) O v)) (g i)) \to (let TMP_147 \def (THead k0 u0 t2) in (let
142 TMP_148 \def (weight_map f TMP_147) in (let TMP_149 \def (THead k0 u0 t1) in
143 (let TMP_150 \def (weight_map g TMP_149) in (le TMP_148
144 TMP_150))))))))))))))))) in (let TMP_287 \def (\lambda (b: B).(let TMP_158
145 \def (\lambda (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1:
146 T).(\forall (i: nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f:
147 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
148 (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind
149 b0) i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
150 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
151 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
152 (let TMP_152 \def (Bind b0) in (let TMP_153 \def (THead TMP_152 u0 t2) in
153 (let TMP_154 \def (weight_map f TMP_153) in (let TMP_155 \def (Bind b0) in
154 (let TMP_156 \def (THead TMP_155 u0 t1) in (let TMP_157 \def (weight_map g
155 TMP_156) in (le TMP_154 TMP_157))))))))))))))))))) in (let TMP_216 \def
156 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
157 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
158 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
159 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
160 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
161 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
162 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let
163 TMP_159 \def (weight_map f u0) in (let TMP_160 \def (weight_map f u0) in (let
164 TMP_161 \def (S TMP_160) in (let TMP_162 \def (wadd f TMP_161) in (let
165 TMP_163 \def (weight_map TMP_162 t2) in (let TMP_164 \def (plus TMP_159
166 TMP_163) in (let TMP_165 \def (weight_map g u0) in (let TMP_166 \def
167 (weight_map g u0) in (let TMP_167 \def (S TMP_166) in (let TMP_168 \def (wadd
168 g TMP_167) in (let TMP_169 \def (weight_map TMP_168 t1) in (let TMP_170 \def
169 (plus TMP_165 TMP_169) in (let TMP_171 \def (weight_map f u0) in (let TMP_172
170 \def (weight_map g u0) in (let TMP_173 \def (weight_map f u0) in (let TMP_174
171 \def (S TMP_173) in (let TMP_175 \def (wadd f TMP_174) in (let TMP_176 \def
172 (weight_map TMP_175 t2) in (let TMP_177 \def (weight_map g u0) in (let
173 TMP_178 \def (S TMP_177) in (let TMP_179 \def (wadd g TMP_178) in (let
174 TMP_180 \def (weight_map TMP_179 t1) in (let TMP_181 \def (weight_le u0 f g
175 H2) in (let TMP_182 \def (weight_map f u0) in (let TMP_183 \def (S TMP_182)
176 in (let TMP_184 \def (wadd f TMP_183) in (let TMP_185 \def (weight_map g u0)
177 in (let TMP_186 \def (S TMP_185) in (let TMP_187 \def (wadd g TMP_186) in
178 (let TMP_196 \def (\lambda (m: nat).(let TMP_188 \def (weight_map f u0) in
179 (let TMP_189 \def (S TMP_188) in (let TMP_190 \def (weight_map g u0) in (let
180 TMP_191 \def (S TMP_190) in (let TMP_192 \def (weight_map f u0) in (let
181 TMP_193 \def (weight_map g u0) in (let TMP_194 \def (weight_le u0 f g H2) in
182 (let TMP_195 \def (le_n_S TMP_192 TMP_193 TMP_194) in (wadd_le f g H2 TMP_189
183 TMP_191 TMP_195 m)))))))))) in (let TMP_197 \def (S i) in (let TMP_198 \def
184 (lift TMP_197 O v) in (let TMP_199 \def (weight_map f TMP_198) in (let
185 TMP_201 \def (\lambda (n: nat).(let TMP_200 \def (g i) in (lt n TMP_200))) in
186 (let TMP_202 \def (weight_map f u0) in (let TMP_203 \def (S TMP_202) in (let
187 TMP_204 \def (wadd f TMP_203) in (let TMP_205 \def (S i) in (let TMP_206 \def
188 (S TMP_205) in (let TMP_207 \def (lift TMP_206 O v) in (let TMP_208 \def
189 (weight_map TMP_204 TMP_207) in (let TMP_209 \def (weight_map f u0) in (let
190 TMP_210 \def (S TMP_209) in (let TMP_211 \def (S i) in (let TMP_212 \def
191 (lift_weight_add_O TMP_210 v TMP_211 f) in (let TMP_213 \def (eq_ind nat
192 TMP_199 TMP_201 H3 TMP_208 TMP_212) in (let TMP_214 \def (H1 TMP_184 TMP_187
193 TMP_196 TMP_213) in (let TMP_215 \def (le_plus_plus TMP_171 TMP_172 TMP_176
194 TMP_180 TMP_181 TMP_214) in (le_n_S TMP_164 TMP_170
195 TMP_215)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let
196 TMP_251 \def (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i:
197 nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat
198 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g
199 m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
200 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
201 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
202 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
203 i))).(let TMP_217 \def (weight_map f u0) in (let TMP_218 \def (wadd f O) in
204 (let TMP_219 \def (weight_map TMP_218 t2) in (let TMP_220 \def (plus TMP_217
205 TMP_219) in (let TMP_221 \def (weight_map g u0) in (let TMP_222 \def (wadd g
206 O) in (let TMP_223 \def (weight_map TMP_222 t1) in (let TMP_224 \def (plus
207 TMP_221 TMP_223) in (let TMP_225 \def (weight_map f u0) in (let TMP_226 \def
208 (weight_map g u0) in (let TMP_227 \def (wadd f O) in (let TMP_228 \def
209 (weight_map TMP_227 t2) in (let TMP_229 \def (wadd g O) in (let TMP_230 \def
210 (weight_map TMP_229 t1) in (let TMP_231 \def (weight_le u0 f g H2) in (let
211 TMP_232 \def (wadd f O) in (let TMP_233 \def (wadd g O) in (let TMP_235 \def
212 (\lambda (m: nat).(let TMP_234 \def (le_O_n O) in (wadd_le f g H2 O O TMP_234
213 m))) in (let TMP_236 \def (S i) in (let TMP_237 \def (lift TMP_236 O v) in
214 (let TMP_238 \def (weight_map f TMP_237) in (let TMP_240 \def (\lambda (n:
215 nat).(let TMP_239 \def (g i) in (lt n TMP_239))) in (let TMP_241 \def (wadd f
216 O) in (let TMP_242 \def (S i) in (let TMP_243 \def (S TMP_242) in (let
217 TMP_244 \def (lift TMP_243 O v) in (let TMP_245 \def (weight_map TMP_241
218 TMP_244) in (let TMP_246 \def (S i) in (let TMP_247 \def (lift_weight_add_O O
219 v TMP_246 f) in (let TMP_248 \def (eq_ind nat TMP_238 TMP_240 H3 TMP_245
220 TMP_247) in (let TMP_249 \def (H1 TMP_232 TMP_233 TMP_235 TMP_248) in (let
221 TMP_250 \def (le_plus_plus TMP_225 TMP_226 TMP_228 TMP_230 TMP_231 TMP_249)
222 in (le_n_S TMP_220 TMP_224
223 TMP_250)))))))))))))))))))))))))))))))))))))))))))) in (let TMP_286 \def
224 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
225 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
226 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
227 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
228 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
229 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
230 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let
231 TMP_252 \def (weight_map f u0) in (let TMP_253 \def (wadd f O) in (let
232 TMP_254 \def (weight_map TMP_253 t2) in (let TMP_255 \def (plus TMP_252
233 TMP_254) in (let TMP_256 \def (weight_map g u0) in (let TMP_257 \def (wadd g
234 O) in (let TMP_258 \def (weight_map TMP_257 t1) in (let TMP_259 \def (plus
235 TMP_256 TMP_258) in (let TMP_260 \def (weight_map f u0) in (let TMP_261 \def
236 (weight_map g u0) in (let TMP_262 \def (wadd f O) in (let TMP_263 \def
237 (weight_map TMP_262 t2) in (let TMP_264 \def (wadd g O) in (let TMP_265 \def
238 (weight_map TMP_264 t1) in (let TMP_266 \def (weight_le u0 f g H2) in (let
239 TMP_267 \def (wadd f O) in (let TMP_268 \def (wadd g O) in (let TMP_270 \def
240 (\lambda (m: nat).(let TMP_269 \def (le_O_n O) in (wadd_le f g H2 O O TMP_269
241 m))) in (let TMP_271 \def (S i) in (let TMP_272 \def (lift TMP_271 O v) in
242 (let TMP_273 \def (weight_map f TMP_272) in (let TMP_275 \def (\lambda (n:
243 nat).(let TMP_274 \def (g i) in (lt n TMP_274))) in (let TMP_276 \def (wadd f
244 O) in (let TMP_277 \def (S i) in (let TMP_278 \def (S TMP_277) in (let
245 TMP_279 \def (lift TMP_278 O v) in (let TMP_280 \def (weight_map TMP_276
246 TMP_279) in (let TMP_281 \def (S i) in (let TMP_282 \def (lift_weight_add_O O
247 v TMP_281 f) in (let TMP_283 \def (eq_ind nat TMP_273 TMP_275 H3 TMP_280
248 TMP_282) in (let TMP_284 \def (H1 TMP_267 TMP_268 TMP_270 TMP_283) in (let
249 TMP_285 \def (le_plus_plus TMP_260 TMP_261 TMP_263 TMP_265 TMP_266 TMP_284)
250 in (le_n_S TMP_255 TMP_259
251 TMP_285)))))))))))))))))))))))))))))))))))))))))))) in (B_ind TMP_158 TMP_216
252 TMP_251 TMP_286 b)))))) in (let TMP_301 \def (\lambda (_: F).(\lambda (v:
253 T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
254 v t1 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat
255 \to nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0
256 (lift (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
257 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
258 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
259 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(let TMP_288 \def
260 (weight_map f0 u0) in (let TMP_289 \def (weight_map f0 t2) in (let TMP_290
261 \def (plus TMP_288 TMP_289) in (let TMP_291 \def (weight_map g u0) in (let
262 TMP_292 \def (weight_map g t1) in (let TMP_293 \def (plus TMP_291 TMP_292) in
263 (let TMP_294 \def (weight_map f0 u0) in (let TMP_295 \def (weight_map g u0)
264 in (let TMP_296 \def (weight_map f0 t2) in (let TMP_297 \def (weight_map g
265 t1) in (let TMP_298 \def (weight_le u0 f0 g H2) in (let TMP_299 \def (H1 f0 g
266 H2 H3) in (let TMP_300 \def (le_plus_plus TMP_294 TMP_295 TMP_296 TMP_297
267 TMP_298 TMP_299) in (le_n_S TMP_290 TMP_293 TMP_300))))))))))))))))))))))))))
268 in (K_ind TMP_151 TMP_287 TMP_301 k))))) in (let TMP_458 \def (\lambda (v:
269 T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (_: (subst0 i
270 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
271 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
272 i) O v)) (g i)) \to (le (weight_map f u2) (weight_map g u1)))))))).(\lambda
273 (k: K).(let TMP_307 \def (\lambda (k0: K).(\forall (t1: T).(\forall (t2:
274 T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall
275 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
276 (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (le (weight_map f
277 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
278 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
279 f (lift (S i) O v)) (g i)) \to (let TMP_303 \def (THead k0 u2 t2) in (let
280 TMP_304 \def (weight_map f TMP_303) in (let TMP_305 \def (THead k0 u1 t1) in
281 (let TMP_306 \def (weight_map g TMP_305) in (le TMP_304 TMP_306))))))))))))))
282 in (let TMP_443 \def (\lambda (b: B).(let TMP_314 \def (\lambda (b0:
283 B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v t1 t2) \to
284 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
285 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O
286 v)) (g (s (Bind b0) i))) \to (le (weight_map f t2) (weight_map g t1)))))))
287 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
288 (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i))
289 \to (let TMP_308 \def (Bind b0) in (let TMP_309 \def (THead TMP_308 u2 t2) in
290 (let TMP_310 \def (weight_map f TMP_309) in (let TMP_311 \def (Bind b0) in
291 (let TMP_312 \def (THead TMP_311 u1 t1) in (let TMP_313 \def (weight_map g
292 TMP_312) in (le TMP_310 TMP_313)))))))))))))))) in (let TMP_372 \def (\lambda
293 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
294 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
295 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
296 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
297 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
298 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
299 i))).(let TMP_315 \def (weight_map f u2) in (let TMP_316 \def (weight_map f
300 u2) in (let TMP_317 \def (S TMP_316) in (let TMP_318 \def (wadd f TMP_317) in
301 (let TMP_319 \def (weight_map TMP_318 t2) in (let TMP_320 \def (plus TMP_315
302 TMP_319) in (let TMP_321 \def (weight_map g u1) in (let TMP_322 \def
303 (weight_map g u1) in (let TMP_323 \def (S TMP_322) in (let TMP_324 \def (wadd
304 g TMP_323) in (let TMP_325 \def (weight_map TMP_324 t1) in (let TMP_326 \def
305 (plus TMP_321 TMP_325) in (let TMP_327 \def (weight_map f u2) in (let TMP_328
306 \def (weight_map g u1) in (let TMP_329 \def (weight_map f u2) in (let TMP_330
307 \def (S TMP_329) in (let TMP_331 \def (wadd f TMP_330) in (let TMP_332 \def
308 (weight_map TMP_331 t2) in (let TMP_333 \def (weight_map g u1) in (let
309 TMP_334 \def (S TMP_333) in (let TMP_335 \def (wadd g TMP_334) in (let
310 TMP_336 \def (weight_map TMP_335 t1) in (let TMP_337 \def (H1 f g H4 H5) in
311 (let TMP_338 \def (weight_map f u2) in (let TMP_339 \def (S TMP_338) in (let
312 TMP_340 \def (wadd f TMP_339) in (let TMP_341 \def (weight_map g u1) in (let
313 TMP_342 \def (S TMP_341) in (let TMP_343 \def (wadd g TMP_342) in (let
314 TMP_352 \def (\lambda (m: nat).(let TMP_344 \def (weight_map f u2) in (let
315 TMP_345 \def (S TMP_344) in (let TMP_346 \def (weight_map g u1) in (let
316 TMP_347 \def (S TMP_346) in (let TMP_348 \def (weight_map f u2) in (let
317 TMP_349 \def (weight_map g u1) in (let TMP_350 \def (H1 f g H4 H5) in (let
318 TMP_351 \def (le_n_S TMP_348 TMP_349 TMP_350) in (wadd_le f g H4 TMP_345
319 TMP_347 TMP_351 m)))))))))) in (let TMP_353 \def (S i) in (let TMP_354 \def
320 (lift TMP_353 O v) in (let TMP_355 \def (weight_map f TMP_354) in (let
321 TMP_357 \def (\lambda (n: nat).(let TMP_356 \def (g i) in (lt n TMP_356))) in
322 (let TMP_358 \def (weight_map f u2) in (let TMP_359 \def (S TMP_358) in (let
323 TMP_360 \def (wadd f TMP_359) in (let TMP_361 \def (S i) in (let TMP_362 \def
324 (S TMP_361) in (let TMP_363 \def (lift TMP_362 O v) in (let TMP_364 \def
325 (weight_map TMP_360 TMP_363) in (let TMP_365 \def (weight_map f u2) in (let
326 TMP_366 \def (S TMP_365) in (let TMP_367 \def (S i) in (let TMP_368 \def
327 (lift_weight_add_O TMP_366 v TMP_367 f) in (let TMP_369 \def (eq_ind nat
328 TMP_355 TMP_357 H5 TMP_364 TMP_368) in (let TMP_370 \def (H3 TMP_340 TMP_343
329 TMP_352 TMP_369) in (let TMP_371 \def (le_plus_plus TMP_327 TMP_328 TMP_332
330 TMP_336 TMP_337 TMP_370) in (le_n_S TMP_320 TMP_326
331 TMP_371))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let
332 TMP_407 \def (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
333 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
334 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
335 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
336 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
337 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
338 (weight_map f (lift (S i) O v)) (g i))).(let TMP_373 \def (weight_map f u2)
339 in (let TMP_374 \def (wadd f O) in (let TMP_375 \def (weight_map TMP_374 t2)
340 in (let TMP_376 \def (plus TMP_373 TMP_375) in (let TMP_377 \def (weight_map
341 g u1) in (let TMP_378 \def (wadd g O) in (let TMP_379 \def (weight_map
342 TMP_378 t1) in (let TMP_380 \def (plus TMP_377 TMP_379) in (let TMP_381 \def
343 (weight_map f u2) in (let TMP_382 \def (weight_map g u1) in (let TMP_383 \def
344 (wadd f O) in (let TMP_384 \def (weight_map TMP_383 t2) in (let TMP_385 \def
345 (wadd g O) in (let TMP_386 \def (weight_map TMP_385 t1) in (let TMP_387 \def
346 (H1 f g H4 H5) in (let TMP_388 \def (wadd f O) in (let TMP_389 \def (wadd g
347 O) in (let TMP_391 \def (\lambda (m: nat).(let TMP_390 \def (le_O_n O) in
348 (wadd_le f g H4 O O TMP_390 m))) in (let TMP_392 \def (S i) in (let TMP_393
349 \def (lift TMP_392 O v) in (let TMP_394 \def (weight_map f TMP_393) in (let
350 TMP_396 \def (\lambda (n: nat).(let TMP_395 \def (g i) in (lt n TMP_395))) in
351 (let TMP_397 \def (wadd f O) in (let TMP_398 \def (S i) in (let TMP_399 \def
352 (S TMP_398) in (let TMP_400 \def (lift TMP_399 O v) in (let TMP_401 \def
353 (weight_map TMP_397 TMP_400) in (let TMP_402 \def (S i) in (let TMP_403 \def
354 (lift_weight_add_O O v TMP_402 f) in (let TMP_404 \def (eq_ind nat TMP_394
355 TMP_396 H5 TMP_401 TMP_403) in (let TMP_405 \def (H3 TMP_388 TMP_389 TMP_391
356 TMP_404) in (let TMP_406 \def (le_plus_plus TMP_381 TMP_382 TMP_384 TMP_386
357 TMP_387 TMP_405) in (le_n_S TMP_376 TMP_380
358 TMP_406))))))))))))))))))))))))))))))))))))))))) in (let TMP_442 \def
359 (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1
360 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
361 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
362 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
363 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
364 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
365 (weight_map f (lift (S i) O v)) (g i))).(let TMP_408 \def (weight_map f u2)
366 in (let TMP_409 \def (wadd f O) in (let TMP_410 \def (weight_map TMP_409 t2)
367 in (let TMP_411 \def (plus TMP_408 TMP_410) in (let TMP_412 \def (weight_map
368 g u1) in (let TMP_413 \def (wadd g O) in (let TMP_414 \def (weight_map
369 TMP_413 t1) in (let TMP_415 \def (plus TMP_412 TMP_414) in (let TMP_416 \def
370 (weight_map f u2) in (let TMP_417 \def (weight_map g u1) in (let TMP_418 \def
371 (wadd f O) in (let TMP_419 \def (weight_map TMP_418 t2) in (let TMP_420 \def
372 (wadd g O) in (let TMP_421 \def (weight_map TMP_420 t1) in (let TMP_422 \def
373 (H1 f g H4 H5) in (let TMP_423 \def (wadd f O) in (let TMP_424 \def (wadd g
374 O) in (let TMP_426 \def (\lambda (m: nat).(let TMP_425 \def (le_O_n O) in
375 (wadd_le f g H4 O O TMP_425 m))) in (let TMP_427 \def (S i) in (let TMP_428
376 \def (lift TMP_427 O v) in (let TMP_429 \def (weight_map f TMP_428) in (let
377 TMP_431 \def (\lambda (n: nat).(let TMP_430 \def (g i) in (lt n TMP_430))) in
378 (let TMP_432 \def (wadd f O) in (let TMP_433 \def (S i) in (let TMP_434 \def
379 (S TMP_433) in (let TMP_435 \def (lift TMP_434 O v) in (let TMP_436 \def
380 (weight_map TMP_432 TMP_435) in (let TMP_437 \def (S i) in (let TMP_438 \def
381 (lift_weight_add_O O v TMP_437 f) in (let TMP_439 \def (eq_ind nat TMP_429
382 TMP_431 H5 TMP_436 TMP_438) in (let TMP_440 \def (H3 TMP_423 TMP_424 TMP_426
383 TMP_439) in (let TMP_441 \def (le_plus_plus TMP_416 TMP_417 TMP_419 TMP_421
384 TMP_422 TMP_440) in (le_n_S TMP_411 TMP_415
385 TMP_441))))))))))))))))))))))))))))))))))))))))) in (B_ind TMP_314 TMP_372
386 TMP_407 TMP_442 b)))))) in (let TMP_457 \def (\lambda (_: F).(\lambda (t1:
387 T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall
388 (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le
389 (f0 m) (g m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le
390 (weight_map f0 t2) (weight_map g t1)))))))).(\lambda (f0: ((nat \to
391 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0
392 m) (g m))))).(\lambda (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(let
393 TMP_444 \def (weight_map f0 u2) in (let TMP_445 \def (weight_map f0 t2) in
394 (let TMP_446 \def (plus TMP_444 TMP_445) in (let TMP_447 \def (weight_map g
395 u1) in (let TMP_448 \def (weight_map g t1) in (let TMP_449 \def (plus TMP_447
396 TMP_448) in (let TMP_450 \def (weight_map f0 u2) in (let TMP_451 \def
397 (weight_map g u1) in (let TMP_452 \def (weight_map f0 t2) in (let TMP_453
398 \def (weight_map g t1) in (let TMP_454 \def (H1 f0 g H4 H5) in (let TMP_455
399 \def (H3 f0 g H4 H5) in (let TMP_456 \def (le_plus_plus TMP_450 TMP_451
400 TMP_452 TMP_453 TMP_454 TMP_455) in (le_n_S TMP_446 TMP_449
401 TMP_456))))))))))))))))))))))) in (K_ind TMP_307 TMP_443 TMP_457 k)))))))))))
402 in (subst0_ind TMP_3 TMP_33 TMP_146 TMP_302 TMP_458 d u t z H)))))))))).
404 theorem subst0_weight_lt:
405 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
406 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
407 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
408 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
410 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
411 (H: (subst0 d u t z)).(let TMP_3 \def (\lambda (n: nat).(\lambda (t0:
412 T).(\lambda (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall
413 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
414 (weight_map f (lift (S n) O t0)) (g n)) \to (let TMP_1 \def (weight_map f t2)
415 in (let TMP_2 \def (weight_map g t1) in (lt TMP_1 TMP_2))))))))))) in (let
416 TMP_4 \def (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to
417 nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f
418 m) (g m))))).(\lambda (H1: (lt (weight_map f (lift (S i) O v)) (g
419 i))).H1)))))) in (let TMP_129 \def (\lambda (v: T).(\lambda (u2: T).(\lambda
420 (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1:
421 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
422 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
423 (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda (t0: T).(\lambda (k:
424 K).(let TMP_9 \def (\lambda (k0: K).(\forall (f: ((nat \to nat))).(\forall
425 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
426 (weight_map f (lift (S i) O v)) (g i)) \to (let TMP_5 \def (THead k0 u2 t0)
427 in (let TMP_6 \def (weight_map f TMP_5) in (let TMP_7 \def (THead k0 u1 t0)
428 in (let TMP_8 \def (weight_map g TMP_7) in (lt TMP_6 TMP_8)))))))))) in (let
429 TMP_114 \def (\lambda (b: B).(let TMP_16 \def (\lambda (b0: B).(\forall (f:
430 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
431 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (let TMP_10 \def
432 (Bind b0) in (let TMP_11 \def (THead TMP_10 u2 t0) in (let TMP_12 \def
433 (weight_map f TMP_11) in (let TMP_13 \def (Bind b0) in (let TMP_14 \def
434 (THead TMP_13 u1 t0) in (let TMP_15 \def (weight_map g TMP_14) in (lt TMP_12
435 TMP_15)))))))))))) in (let TMP_57 \def (\lambda (f: ((nat \to nat))).(\lambda
436 (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
437 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let TMP_17
438 \def (weight_map f u2) in (let TMP_18 \def (weight_map f u2) in (let TMP_19
439 \def (S TMP_18) in (let TMP_20 \def (wadd f TMP_19) in (let TMP_21 \def
440 (weight_map TMP_20 t0) in (let TMP_22 \def (plus TMP_17 TMP_21) in (let
441 TMP_23 \def (weight_map g u1) in (let TMP_24 \def (weight_map g u1) in (let
442 TMP_25 \def (S TMP_24) in (let TMP_26 \def (wadd g TMP_25) in (let TMP_27
443 \def (weight_map TMP_26 t0) in (let TMP_28 \def (plus TMP_23 TMP_27) in (let
444 TMP_29 \def (weight_map f u2) in (let TMP_30 \def (weight_map g u1) in (let
445 TMP_31 \def (weight_map f u2) in (let TMP_32 \def (S TMP_31) in (let TMP_33
446 \def (wadd f TMP_32) in (let TMP_34 \def (weight_map TMP_33 t0) in (let
447 TMP_35 \def (weight_map g u1) in (let TMP_36 \def (S TMP_35) in (let TMP_37
448 \def (wadd g TMP_36) in (let TMP_38 \def (weight_map TMP_37 t0) in (let
449 TMP_39 \def (H1 f g H2 H3) in (let TMP_40 \def (weight_map f u2) in (let
450 TMP_41 \def (S TMP_40) in (let TMP_42 \def (wadd f TMP_41) in (let TMP_43
451 \def (weight_map g u1) in (let TMP_44 \def (S TMP_43) in (let TMP_45 \def
452 (wadd g TMP_44) in (let TMP_54 \def (\lambda (n: nat).(let TMP_46 \def
453 (weight_map f u2) in (let TMP_47 \def (S TMP_46) in (let TMP_48 \def
454 (weight_map g u1) in (let TMP_49 \def (S TMP_48) in (let TMP_50 \def
455 (weight_map f u2) in (let TMP_51 \def (weight_map g u1) in (let TMP_52 \def
456 (H1 f g H2 H3) in (let TMP_53 \def (lt_n_S TMP_50 TMP_51 TMP_52) in (wadd_lt
457 f g H2 TMP_47 TMP_49 TMP_53 n)))))))))) in (let TMP_55 \def (weight_le t0
458 TMP_42 TMP_45 TMP_54) in (let TMP_56 \def (lt_le_plus_plus TMP_29 TMP_30
459 TMP_34 TMP_38 TMP_39 TMP_55) in (lt_n_S TMP_22 TMP_28
460 TMP_56))))))))))))))))))))))))))))))))))))) in (let TMP_85 \def (\lambda (f:
461 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
462 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
463 i))).(let TMP_58 \def (weight_map f u2) in (let TMP_59 \def (wadd f O) in
464 (let TMP_60 \def (weight_map TMP_59 t0) in (let TMP_61 \def (plus TMP_58
465 TMP_60) in (let TMP_62 \def (weight_map g u1) in (let TMP_63 \def (wadd g O)
466 in (let TMP_64 \def (weight_map TMP_63 t0) in (let TMP_65 \def (plus TMP_62
467 TMP_64) in (let TMP_66 \def (weight_map f u2) in (let TMP_67 \def (weight_map
468 g u1) in (let TMP_68 \def (wadd f O) in (let TMP_69 \def (weight_map TMP_68
469 t0) in (let TMP_70 \def (wadd g O) in (let TMP_71 \def (weight_map TMP_70 t0)
470 in (let TMP_72 \def (H1 f g H2 H3) in (let TMP_73 \def (wadd f O) in (let
471 TMP_74 \def (wadd g O) in (let TMP_82 \def (\lambda (n: nat).(let TMP_75 \def
472 (wadd f O n) in (let TMP_76 \def (wadd g O n) in (let TMP_77 \def (wadd f O
473 n) in (let TMP_78 \def (wadd g O n) in (let TMP_79 \def (le_O_n O) in (let
474 TMP_80 \def (wadd_le f g H2 O O TMP_79 n) in (let TMP_81 \def (le_n_S TMP_77
475 TMP_78 TMP_80) in (le_S_n TMP_75 TMP_76 TMP_81))))))))) in (let TMP_83 \def
476 (weight_le t0 TMP_73 TMP_74 TMP_82) in (let TMP_84 \def (lt_le_plus_plus
477 TMP_66 TMP_67 TMP_69 TMP_71 TMP_72 TMP_83) in (lt_n_S TMP_61 TMP_65
478 TMP_84))))))))))))))))))))))))) in (let TMP_113 \def (\lambda (f: ((nat \to
479 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
480 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let
481 TMP_86 \def (weight_map f u2) in (let TMP_87 \def (wadd f O) in (let TMP_88
482 \def (weight_map TMP_87 t0) in (let TMP_89 \def (plus TMP_86 TMP_88) in (let
483 TMP_90 \def (weight_map g u1) in (let TMP_91 \def (wadd g O) in (let TMP_92
484 \def (weight_map TMP_91 t0) in (let TMP_93 \def (plus TMP_90 TMP_92) in (let
485 TMP_94 \def (weight_map f u2) in (let TMP_95 \def (weight_map g u1) in (let
486 TMP_96 \def (wadd f O) in (let TMP_97 \def (weight_map TMP_96 t0) in (let
487 TMP_98 \def (wadd g O) in (let TMP_99 \def (weight_map TMP_98 t0) in (let
488 TMP_100 \def (H1 f g H2 H3) in (let TMP_101 \def (wadd f O) in (let TMP_102
489 \def (wadd g O) in (let TMP_110 \def (\lambda (n: nat).(let TMP_103 \def
490 (wadd f O n) in (let TMP_104 \def (wadd g O n) in (let TMP_105 \def (wadd f O
491 n) in (let TMP_106 \def (wadd g O n) in (let TMP_107 \def (le_O_n O) in (let
492 TMP_108 \def (wadd_le f g H2 O O TMP_107 n) in (let TMP_109 \def (le_n_S
493 TMP_105 TMP_106 TMP_108) in (le_S_n TMP_103 TMP_104 TMP_109))))))))) in (let
494 TMP_111 \def (weight_le t0 TMP_101 TMP_102 TMP_110) in (let TMP_112 \def
495 (lt_le_plus_plus TMP_94 TMP_95 TMP_97 TMP_99 TMP_100 TMP_111) in (lt_n_S
496 TMP_89 TMP_93 TMP_112))))))))))))))))))))))))) in (B_ind TMP_16 TMP_57 TMP_85
497 TMP_113 b)))))) in (let TMP_128 \def (\lambda (_: F).(\lambda (f0: ((nat \to
498 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
499 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(let
500 TMP_115 \def (weight_map f0 u2) in (let TMP_116 \def (weight_map f0 t0) in
501 (let TMP_117 \def (plus TMP_115 TMP_116) in (let TMP_118 \def (weight_map g
502 u1) in (let TMP_119 \def (weight_map g t0) in (let TMP_120 \def (plus TMP_118
503 TMP_119) in (let TMP_121 \def (weight_map f0 u2) in (let TMP_122 \def
504 (weight_map g u1) in (let TMP_123 \def (weight_map f0 t0) in (let TMP_124
505 \def (weight_map g t0) in (let TMP_125 \def (H1 f0 g H2 H3) in (let TMP_126
506 \def (weight_le t0 f0 g H2) in (let TMP_127 \def (lt_le_plus_plus TMP_121
507 TMP_122 TMP_123 TMP_124 TMP_125 TMP_126) in (lt_n_S TMP_117 TMP_120
508 TMP_127))))))))))))))))))) in (K_ind TMP_9 TMP_114 TMP_128 k)))))))))))) in
509 (let TMP_285 \def (\lambda (k: K).(let TMP_134 \def (\lambda (k0: K).(\forall
510 (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i)
511 v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
512 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
513 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
514 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
515 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
516 f (lift (S i) O v)) (g i)) \to (let TMP_130 \def (THead k0 u0 t2) in (let
517 TMP_131 \def (weight_map f TMP_130) in (let TMP_132 \def (THead k0 u0 t1) in
518 (let TMP_133 \def (weight_map g TMP_132) in (lt TMP_131
519 TMP_133))))))))))))))))) in (let TMP_270 \def (\lambda (b: B).(let TMP_141
520 \def (\lambda (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1:
521 T).(\forall (i: nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f:
522 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
523 (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind
524 b0) i))) \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
525 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
526 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
527 (let TMP_135 \def (Bind b0) in (let TMP_136 \def (THead TMP_135 u0 t2) in
528 (let TMP_137 \def (weight_map f TMP_136) in (let TMP_138 \def (Bind b0) in
529 (let TMP_139 \def (THead TMP_138 u0 t1) in (let TMP_140 \def (weight_map g
530 TMP_139) in (lt TMP_137 TMP_140))))))))))))))))))) in (let TMP_199 \def
531 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
532 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
533 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
534 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
535 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
536 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
537 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let
538 TMP_142 \def (weight_map f u0) in (let TMP_143 \def (weight_map f u0) in (let
539 TMP_144 \def (S TMP_143) in (let TMP_145 \def (wadd f TMP_144) in (let
540 TMP_146 \def (weight_map TMP_145 t2) in (let TMP_147 \def (plus TMP_142
541 TMP_146) in (let TMP_148 \def (weight_map g u0) in (let TMP_149 \def
542 (weight_map g u0) in (let TMP_150 \def (S TMP_149) in (let TMP_151 \def (wadd
543 g TMP_150) in (let TMP_152 \def (weight_map TMP_151 t1) in (let TMP_153 \def
544 (plus TMP_148 TMP_152) in (let TMP_154 \def (weight_map f u0) in (let TMP_155
545 \def (weight_map g u0) in (let TMP_156 \def (weight_map f u0) in (let TMP_157
546 \def (S TMP_156) in (let TMP_158 \def (wadd f TMP_157) in (let TMP_159 \def
547 (weight_map TMP_158 t2) in (let TMP_160 \def (weight_map g u0) in (let
548 TMP_161 \def (S TMP_160) in (let TMP_162 \def (wadd g TMP_161) in (let
549 TMP_163 \def (weight_map TMP_162 t1) in (let TMP_164 \def (weight_le u0 f g
550 H2) in (let TMP_165 \def (weight_map f u0) in (let TMP_166 \def (S TMP_165)
551 in (let TMP_167 \def (wadd f TMP_166) in (let TMP_168 \def (weight_map g u0)
552 in (let TMP_169 \def (S TMP_168) in (let TMP_170 \def (wadd g TMP_169) in
553 (let TMP_179 \def (\lambda (m: nat).(let TMP_171 \def (weight_map f u0) in
554 (let TMP_172 \def (S TMP_171) in (let TMP_173 \def (weight_map g u0) in (let
555 TMP_174 \def (S TMP_173) in (let TMP_175 \def (weight_map f u0) in (let
556 TMP_176 \def (weight_map g u0) in (let TMP_177 \def (weight_le u0 f g H2) in
557 (let TMP_178 \def (le_n_S TMP_175 TMP_176 TMP_177) in (wadd_le f g H2 TMP_172
558 TMP_174 TMP_178 m)))))))))) in (let TMP_180 \def (S i) in (let TMP_181 \def
559 (lift TMP_180 O v) in (let TMP_182 \def (weight_map f TMP_181) in (let
560 TMP_184 \def (\lambda (n: nat).(let TMP_183 \def (g i) in (lt n TMP_183))) in
561 (let TMP_185 \def (weight_map f u0) in (let TMP_186 \def (S TMP_185) in (let
562 TMP_187 \def (wadd f TMP_186) in (let TMP_188 \def (S i) in (let TMP_189 \def
563 (S TMP_188) in (let TMP_190 \def (lift TMP_189 O v) in (let TMP_191 \def
564 (weight_map TMP_187 TMP_190) in (let TMP_192 \def (weight_map f u0) in (let
565 TMP_193 \def (S TMP_192) in (let TMP_194 \def (S i) in (let TMP_195 \def
566 (lift_weight_add_O TMP_193 v TMP_194 f) in (let TMP_196 \def (eq_ind nat
567 TMP_182 TMP_184 H3 TMP_191 TMP_195) in (let TMP_197 \def (H1 TMP_167 TMP_170
568 TMP_179 TMP_196) in (let TMP_198 \def (le_lt_plus_plus TMP_154 TMP_155
569 TMP_159 TMP_163 TMP_164 TMP_197) in (lt_n_S TMP_147 TMP_153
570 TMP_198)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let
571 TMP_234 \def (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i:
572 nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat
573 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g
574 m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
575 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
576 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
577 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
578 i))).(let TMP_200 \def (weight_map f u0) in (let TMP_201 \def (wadd f O) in
579 (let TMP_202 \def (weight_map TMP_201 t2) in (let TMP_203 \def (plus TMP_200
580 TMP_202) in (let TMP_204 \def (weight_map g u0) in (let TMP_205 \def (wadd g
581 O) in (let TMP_206 \def (weight_map TMP_205 t1) in (let TMP_207 \def (plus
582 TMP_204 TMP_206) in (let TMP_208 \def (weight_map f u0) in (let TMP_209 \def
583 (weight_map g u0) in (let TMP_210 \def (wadd f O) in (let TMP_211 \def
584 (weight_map TMP_210 t2) in (let TMP_212 \def (wadd g O) in (let TMP_213 \def
585 (weight_map TMP_212 t1) in (let TMP_214 \def (weight_le u0 f g H2) in (let
586 TMP_215 \def (wadd f O) in (let TMP_216 \def (wadd g O) in (let TMP_218 \def
587 (\lambda (m: nat).(let TMP_217 \def (le_O_n O) in (wadd_le f g H2 O O TMP_217
588 m))) in (let TMP_219 \def (S i) in (let TMP_220 \def (lift TMP_219 O v) in
589 (let TMP_221 \def (weight_map f TMP_220) in (let TMP_223 \def (\lambda (n:
590 nat).(let TMP_222 \def (g i) in (lt n TMP_222))) in (let TMP_224 \def (wadd f
591 O) in (let TMP_225 \def (S i) in (let TMP_226 \def (S TMP_225) in (let
592 TMP_227 \def (lift TMP_226 O v) in (let TMP_228 \def (weight_map TMP_224
593 TMP_227) in (let TMP_229 \def (S i) in (let TMP_230 \def (lift_weight_add_O O
594 v TMP_229 f) in (let TMP_231 \def (eq_ind nat TMP_221 TMP_223 H3 TMP_228
595 TMP_230) in (let TMP_232 \def (H1 TMP_215 TMP_216 TMP_218 TMP_231) in (let
596 TMP_233 \def (le_lt_plus_plus TMP_208 TMP_209 TMP_211 TMP_213 TMP_214
597 TMP_232) in (lt_n_S TMP_203 TMP_207
598 TMP_233)))))))))))))))))))))))))))))))))))))))))))) in (let TMP_269 \def
599 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
600 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
601 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
602 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
603 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
604 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
605 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(let
606 TMP_235 \def (weight_map f u0) in (let TMP_236 \def (wadd f O) in (let
607 TMP_237 \def (weight_map TMP_236 t2) in (let TMP_238 \def (plus TMP_235
608 TMP_237) in (let TMP_239 \def (weight_map g u0) in (let TMP_240 \def (wadd g
609 O) in (let TMP_241 \def (weight_map TMP_240 t1) in (let TMP_242 \def (plus
610 TMP_239 TMP_241) in (let TMP_243 \def (weight_map f u0) in (let TMP_244 \def
611 (weight_map g u0) in (let TMP_245 \def (wadd f O) in (let TMP_246 \def
612 (weight_map TMP_245 t2) in (let TMP_247 \def (wadd g O) in (let TMP_248 \def
613 (weight_map TMP_247 t1) in (let TMP_249 \def (weight_le u0 f g H2) in (let
614 TMP_250 \def (wadd f O) in (let TMP_251 \def (wadd g O) in (let TMP_253 \def
615 (\lambda (m: nat).(let TMP_252 \def (le_O_n O) in (wadd_le f g H2 O O TMP_252
616 m))) in (let TMP_254 \def (S i) in (let TMP_255 \def (lift TMP_254 O v) in
617 (let TMP_256 \def (weight_map f TMP_255) in (let TMP_258 \def (\lambda (n:
618 nat).(let TMP_257 \def (g i) in (lt n TMP_257))) in (let TMP_259 \def (wadd f
619 O) in (let TMP_260 \def (S i) in (let TMP_261 \def (S TMP_260) in (let
620 TMP_262 \def (lift TMP_261 O v) in (let TMP_263 \def (weight_map TMP_259
621 TMP_262) in (let TMP_264 \def (S i) in (let TMP_265 \def (lift_weight_add_O O
622 v TMP_264 f) in (let TMP_266 \def (eq_ind nat TMP_256 TMP_258 H3 TMP_263
623 TMP_265) in (let TMP_267 \def (H1 TMP_250 TMP_251 TMP_253 TMP_266) in (let
624 TMP_268 \def (le_lt_plus_plus TMP_243 TMP_244 TMP_246 TMP_248 TMP_249
625 TMP_267) in (lt_n_S TMP_238 TMP_242
626 TMP_268)))))))))))))))))))))))))))))))))))))))))))) in (B_ind TMP_141 TMP_199
627 TMP_234 TMP_269 b)))))) in (let TMP_284 \def (\lambda (_: F).(\lambda (v:
628 T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
629 v t1 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat
630 \to nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0
631 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
632 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
633 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
634 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(let TMP_271 \def
635 (weight_map f0 u0) in (let TMP_272 \def (weight_map f0 t2) in (let TMP_273
636 \def (plus TMP_271 TMP_272) in (let TMP_274 \def (weight_map g u0) in (let
637 TMP_275 \def (weight_map g t1) in (let TMP_276 \def (plus TMP_274 TMP_275) in
638 (let TMP_277 \def (weight_map f0 u0) in (let TMP_278 \def (weight_map g u0)
639 in (let TMP_279 \def (weight_map f0 t2) in (let TMP_280 \def (weight_map g
640 t1) in (let TMP_281 \def (weight_le u0 f0 g H2) in (let TMP_282 \def (H1 f0 g
641 H2 H3) in (let TMP_283 \def (le_lt_plus_plus TMP_277 TMP_278 TMP_279 TMP_280
642 TMP_281 TMP_282) in (lt_n_S TMP_273 TMP_276 TMP_283))))))))))))))))))))))))))
643 in (K_ind TMP_134 TMP_270 TMP_284 k))))) in (let TMP_454 \def (\lambda (v:
644 T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (_: (subst0 i
645 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
646 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
647 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
648 (k: K).(let TMP_290 \def (\lambda (k0: K).(\forall (t1: T).(\forall (t2:
649 T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall
650 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
651 (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f
652 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
653 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
654 f (lift (S i) O v)) (g i)) \to (let TMP_286 \def (THead k0 u2 t2) in (let
655 TMP_287 \def (weight_map f TMP_286) in (let TMP_288 \def (THead k0 u1 t1) in
656 (let TMP_289 \def (weight_map g TMP_288) in (lt TMP_287 TMP_289))))))))))))))
657 in (let TMP_439 \def (\lambda (b: B).(let TMP_297 \def (\lambda (b0:
658 B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v t1 t2) \to
659 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
660 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O
661 v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2) (weight_map g t1)))))))
662 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
663 (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i))
664 \to (let TMP_291 \def (Bind b0) in (let TMP_292 \def (THead TMP_291 u2 t2) in
665 (let TMP_293 \def (weight_map f TMP_292) in (let TMP_294 \def (Bind b0) in
666 (let TMP_295 \def (THead TMP_294 u1 t1) in (let TMP_296 \def (weight_map g
667 TMP_295) in (lt TMP_293 TMP_296)))))))))))))))) in (let TMP_356 \def (\lambda
668 (t1: T).(\lambda (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_:
669 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
670 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
671 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
672 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
673 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
674 i))).(let TMP_298 \def (weight_map f u2) in (let TMP_299 \def (weight_map f
675 u2) in (let TMP_300 \def (S TMP_299) in (let TMP_301 \def (wadd f TMP_300) in
676 (let TMP_302 \def (weight_map TMP_301 t2) in (let TMP_303 \def (plus TMP_298
677 TMP_302) in (let TMP_304 \def (weight_map g u1) in (let TMP_305 \def
678 (weight_map g u1) in (let TMP_306 \def (S TMP_305) in (let TMP_307 \def (wadd
679 g TMP_306) in (let TMP_308 \def (weight_map TMP_307 t1) in (let TMP_309 \def
680 (plus TMP_304 TMP_308) in (let TMP_310 \def (weight_map f u2) in (let TMP_311
681 \def (weight_map g u1) in (let TMP_312 \def (weight_map f u2) in (let TMP_313
682 \def (S TMP_312) in (let TMP_314 \def (wadd f TMP_313) in (let TMP_315 \def
683 (weight_map TMP_314 t2) in (let TMP_316 \def (weight_map g u1) in (let
684 TMP_317 \def (S TMP_316) in (let TMP_318 \def (wadd g TMP_317) in (let
685 TMP_319 \def (weight_map TMP_318 t1) in (let TMP_320 \def (H1 f g H4 H5) in
686 (let TMP_321 \def (S i) in (let TMP_322 \def (weight_map f u2) in (let
687 TMP_323 \def (S TMP_322) in (let TMP_324 \def (wadd f TMP_323) in (let
688 TMP_325 \def (weight_map g u1) in (let TMP_326 \def (S TMP_325) in (let
689 TMP_327 \def (wadd g TMP_326) in (let TMP_336 \def (\lambda (m: nat).(let
690 TMP_328 \def (weight_map f u2) in (let TMP_329 \def (S TMP_328) in (let
691 TMP_330 \def (weight_map g u1) in (let TMP_331 \def (S TMP_330) in (let
692 TMP_332 \def (weight_map f u2) in (let TMP_333 \def (weight_map g u1) in (let
693 TMP_334 \def (H1 f g H4 H5) in (let TMP_335 \def (lt_n_S TMP_332 TMP_333
694 TMP_334) in (wadd_lt f g H4 TMP_329 TMP_331 TMP_335 m)))))))))) in (let
695 TMP_337 \def (S i) in (let TMP_338 \def (lift TMP_337 O v) in (let TMP_339
696 \def (weight_map f TMP_338) in (let TMP_341 \def (\lambda (n: nat).(let
697 TMP_340 \def (g i) in (lt n TMP_340))) in (let TMP_342 \def (weight_map f u2)
698 in (let TMP_343 \def (S TMP_342) in (let TMP_344 \def (wadd f TMP_343) in
699 (let TMP_345 \def (S i) in (let TMP_346 \def (S TMP_345) in (let TMP_347 \def
700 (lift TMP_346 O v) in (let TMP_348 \def (weight_map TMP_344 TMP_347) in (let
701 TMP_349 \def (weight_map f u2) in (let TMP_350 \def (S TMP_349) in (let
702 TMP_351 \def (S i) in (let TMP_352 \def (lift_weight_add_O TMP_350 v TMP_351
703 f) in (let TMP_353 \def (eq_ind nat TMP_339 TMP_341 H5 TMP_348 TMP_352) in
704 (let TMP_354 \def (subst0_weight_le v t1 t2 TMP_321 H2 TMP_324 TMP_327
705 TMP_336 TMP_353) in (let TMP_355 \def (lt_le_plus_plus TMP_310 TMP_311
706 TMP_315 TMP_319 TMP_320 TMP_354) in (lt_n_S TMP_303 TMP_309
707 TMP_355)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let
708 TMP_397 \def (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
709 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
710 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
711 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
712 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
713 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
714 (weight_map f (lift (S i) O v)) (g i))).(let TMP_357 \def (weight_map f u2)
715 in (let TMP_358 \def (wadd f O) in (let TMP_359 \def (weight_map TMP_358 t2)
716 in (let TMP_360 \def (plus TMP_357 TMP_359) in (let TMP_361 \def (weight_map
717 g u1) in (let TMP_362 \def (wadd g O) in (let TMP_363 \def (weight_map
718 TMP_362 t1) in (let TMP_364 \def (plus TMP_361 TMP_363) in (let TMP_365 \def
719 (weight_map f u2) in (let TMP_366 \def (weight_map g u1) in (let TMP_367 \def
720 (wadd f O) in (let TMP_368 \def (weight_map TMP_367 t2) in (let TMP_369 \def
721 (wadd g O) in (let TMP_370 \def (weight_map TMP_369 t1) in (let TMP_371 \def
722 (H1 f g H4 H5) in (let TMP_372 \def (wadd f O) in (let TMP_373 \def (wadd g
723 O) in (let TMP_381 \def (\lambda (m: nat).(let TMP_374 \def (wadd f O m) in
724 (let TMP_375 \def (wadd g O m) in (let TMP_376 \def (wadd f O m) in (let
725 TMP_377 \def (wadd g O m) in (let TMP_378 \def (le_O_n O) in (let TMP_379
726 \def (wadd_le f g H4 O O TMP_378 m) in (let TMP_380 \def (le_n_S TMP_376
727 TMP_377 TMP_379) in (le_S_n TMP_374 TMP_375 TMP_380))))))))) in (let TMP_382
728 \def (S i) in (let TMP_383 \def (lift TMP_382 O v) in (let TMP_384 \def
729 (weight_map f TMP_383) in (let TMP_386 \def (\lambda (n: nat).(let TMP_385
730 \def (g i) in (lt n TMP_385))) in (let TMP_387 \def (wadd f O) in (let
731 TMP_388 \def (S i) in (let TMP_389 \def (S TMP_388) in (let TMP_390 \def
732 (lift TMP_389 O v) in (let TMP_391 \def (weight_map TMP_387 TMP_390) in (let
733 TMP_392 \def (S i) in (let TMP_393 \def (lift_weight_add_O O v TMP_392 f) in
734 (let TMP_394 \def (eq_ind nat TMP_384 TMP_386 H5 TMP_391 TMP_393) in (let
735 TMP_395 \def (H3 TMP_372 TMP_373 TMP_381 TMP_394) in (let TMP_396 \def
736 (lt_plus_plus TMP_365 TMP_366 TMP_368 TMP_370 TMP_371 TMP_395) in (lt_n_S
737 TMP_360 TMP_364 TMP_396))))))))))))))))))))))))))))))))))))))))) in (let
738 TMP_438 \def (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
739 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
740 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
741 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
742 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
743 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
744 (weight_map f (lift (S i) O v)) (g i))).(let TMP_398 \def (weight_map f u2)
745 in (let TMP_399 \def (wadd f O) in (let TMP_400 \def (weight_map TMP_399 t2)
746 in (let TMP_401 \def (plus TMP_398 TMP_400) in (let TMP_402 \def (weight_map
747 g u1) in (let TMP_403 \def (wadd g O) in (let TMP_404 \def (weight_map
748 TMP_403 t1) in (let TMP_405 \def (plus TMP_402 TMP_404) in (let TMP_406 \def
749 (weight_map f u2) in (let TMP_407 \def (weight_map g u1) in (let TMP_408 \def
750 (wadd f O) in (let TMP_409 \def (weight_map TMP_408 t2) in (let TMP_410 \def
751 (wadd g O) in (let TMP_411 \def (weight_map TMP_410 t1) in (let TMP_412 \def
752 (H1 f g H4 H5) in (let TMP_413 \def (wadd f O) in (let TMP_414 \def (wadd g
753 O) in (let TMP_422 \def (\lambda (m: nat).(let TMP_415 \def (wadd f O m) in
754 (let TMP_416 \def (wadd g O m) in (let TMP_417 \def (wadd f O m) in (let
755 TMP_418 \def (wadd g O m) in (let TMP_419 \def (le_O_n O) in (let TMP_420
756 \def (wadd_le f g H4 O O TMP_419 m) in (let TMP_421 \def (le_n_S TMP_417
757 TMP_418 TMP_420) in (le_S_n TMP_415 TMP_416 TMP_421))))))))) in (let TMP_423
758 \def (S i) in (let TMP_424 \def (lift TMP_423 O v) in (let TMP_425 \def
759 (weight_map f TMP_424) in (let TMP_427 \def (\lambda (n: nat).(let TMP_426
760 \def (g i) in (lt n TMP_426))) in (let TMP_428 \def (wadd f O) in (let
761 TMP_429 \def (S i) in (let TMP_430 \def (S TMP_429) in (let TMP_431 \def
762 (lift TMP_430 O v) in (let TMP_432 \def (weight_map TMP_428 TMP_431) in (let
763 TMP_433 \def (S i) in (let TMP_434 \def (lift_weight_add_O O v TMP_433 f) in
764 (let TMP_435 \def (eq_ind nat TMP_425 TMP_427 H5 TMP_432 TMP_434) in (let
765 TMP_436 \def (H3 TMP_413 TMP_414 TMP_422 TMP_435) in (let TMP_437 \def
766 (lt_plus_plus TMP_406 TMP_407 TMP_409 TMP_411 TMP_412 TMP_436) in (lt_n_S
767 TMP_401 TMP_405 TMP_437))))))))))))))))))))))))))))))))))))))))) in (B_ind
768 TMP_297 TMP_356 TMP_397 TMP_438 b)))))) in (let TMP_453 \def (\lambda (_:
769 F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1
770 t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
771 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
772 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
773 t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
774 nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5:
775 (lt (weight_map f0 (lift (S i) O v)) (g i))).(let TMP_440 \def (weight_map f0
776 u2) in (let TMP_441 \def (weight_map f0 t2) in (let TMP_442 \def (plus
777 TMP_440 TMP_441) in (let TMP_443 \def (weight_map g u1) in (let TMP_444 \def
778 (weight_map g t1) in (let TMP_445 \def (plus TMP_443 TMP_444) in (let TMP_446
779 \def (weight_map f0 u2) in (let TMP_447 \def (weight_map g u1) in (let
780 TMP_448 \def (weight_map f0 t2) in (let TMP_449 \def (weight_map g t1) in
781 (let TMP_450 \def (H1 f0 g H4 H5) in (let TMP_451 \def (H3 f0 g H4 H5) in
782 (let TMP_452 \def (lt_plus_plus TMP_446 TMP_447 TMP_448 TMP_449 TMP_450
783 TMP_451) in (lt_n_S TMP_442 TMP_445 TMP_452))))))))))))))))))))))) in (K_ind
784 TMP_290 TMP_439 TMP_453 k))))))))))) in (subst0_ind TMP_3 TMP_4 TMP_129
785 TMP_285 TMP_454 d u t z H)))))))))).
787 theorem subst0_tlt_head:
788 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
789 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
791 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
792 z)).(let TMP_1 \def (\lambda (_: nat).O) in (let TMP_2 \def (weight_map TMP_1
793 u) in (let TMP_3 \def (\lambda (_: nat).O) in (let TMP_4 \def (\lambda (_:
794 nat).O) in (let TMP_5 \def (weight_map TMP_4 u) in (let TMP_6 \def (S TMP_5)
795 in (let TMP_7 \def (wadd TMP_3 TMP_6) in (let TMP_8 \def (weight_map TMP_7 z)
796 in (let TMP_9 \def (plus TMP_2 TMP_8) in (let TMP_10 \def (\lambda (_:
797 nat).O) in (let TMP_11 \def (weight_map TMP_10 u) in (let TMP_12 \def
798 (\lambda (_: nat).O) in (let TMP_13 \def (\lambda (_: nat).O) in (let TMP_14
799 \def (weight_map TMP_13 u) in (let TMP_15 \def (S TMP_14) in (let TMP_16 \def
800 (wadd TMP_12 TMP_15) in (let TMP_17 \def (weight_map TMP_16 t) in (let TMP_18
801 \def (plus TMP_11 TMP_17) in (let TMP_19 \def (\lambda (_: nat).O) in (let
802 TMP_20 \def (weight_map TMP_19 u) in (let TMP_21 \def (\lambda (_: nat).O) in
803 (let TMP_22 \def (weight_map TMP_21 u) in (let TMP_23 \def (\lambda (_:
804 nat).O) in (let TMP_24 \def (\lambda (_: nat).O) in (let TMP_25 \def
805 (weight_map TMP_24 u) in (let TMP_26 \def (S TMP_25) in (let TMP_27 \def
806 (wadd TMP_23 TMP_26) in (let TMP_28 \def (weight_map TMP_27 z) in (let TMP_29
807 \def (\lambda (_: nat).O) in (let TMP_30 \def (\lambda (_: nat).O) in (let
808 TMP_31 \def (weight_map TMP_30 u) in (let TMP_32 \def (S TMP_31) in (let
809 TMP_33 \def (wadd TMP_29 TMP_32) in (let TMP_34 \def (weight_map TMP_33 t) in
810 (let TMP_35 \def (\lambda (_: nat).O) in (let TMP_36 \def (weight_map TMP_35
811 u) in (let TMP_37 \def (le_n TMP_36) in (let TMP_38 \def (\lambda (_: nat).O)
812 in (let TMP_39 \def (\lambda (_: nat).O) in (let TMP_40 \def (weight_map
813 TMP_39 u) in (let TMP_41 \def (S TMP_40) in (let TMP_42 \def (wadd TMP_38
814 TMP_41) in (let TMP_43 \def (\lambda (_: nat).O) in (let TMP_44 \def (\lambda
815 (_: nat).O) in (let TMP_45 \def (weight_map TMP_44 u) in (let TMP_46 \def (S
816 TMP_45) in (let TMP_47 \def (wadd TMP_43 TMP_46) in (let TMP_53 \def (\lambda
817 (m: nat).(let TMP_48 \def (\lambda (_: nat).O) in (let TMP_49 \def (\lambda
818 (_: nat).O) in (let TMP_50 \def (weight_map TMP_49 u) in (let TMP_51 \def (S
819 TMP_50) in (let TMP_52 \def (wadd TMP_48 TMP_51 m) in (le_n TMP_52))))))) in
820 (let TMP_54 \def (\lambda (_: nat).O) in (let TMP_55 \def (lift O O u) in
821 (let TMP_56 \def (weight_map TMP_54 TMP_55) in (let TMP_60 \def (\lambda (n:
822 nat).(let TMP_57 \def (\lambda (_: nat).O) in (let TMP_58 \def (weight_map
823 TMP_57 u) in (let TMP_59 \def (S TMP_58) in (lt n TMP_59))))) in (let TMP_66
824 \def (\lambda (t0: T).(let TMP_61 \def (\lambda (_: nat).O) in (let TMP_62
825 \def (weight_map TMP_61 t0) in (let TMP_63 \def (\lambda (_: nat).O) in (let
826 TMP_64 \def (weight_map TMP_63 u) in (let TMP_65 \def (S TMP_64) in (lt
827 TMP_62 TMP_65))))))) in (let TMP_67 \def (\lambda (_: nat).O) in (let TMP_68
828 \def (weight_map TMP_67 u) in (let TMP_69 \def (S TMP_68) in (let TMP_70 \def
829 (le_n TMP_69) in (let TMP_71 \def (lift O O u) in (let TMP_72 \def (lift_r u
830 O) in (let TMP_73 \def (eq_ind_r T u TMP_66 TMP_70 TMP_71 TMP_72) in (let
831 TMP_74 \def (\lambda (_: nat).O) in (let TMP_75 \def (\lambda (_: nat).O) in
832 (let TMP_76 \def (weight_map TMP_75 u) in (let TMP_77 \def (S TMP_76) in (let
833 TMP_78 \def (wadd TMP_74 TMP_77) in (let TMP_79 \def (S O) in (let TMP_80
834 \def (lift TMP_79 O u) in (let TMP_81 \def (weight_map TMP_78 TMP_80) in (let
835 TMP_82 \def (\lambda (_: nat).O) in (let TMP_83 \def (weight_map TMP_82 u) in
836 (let TMP_84 \def (S TMP_83) in (let TMP_85 \def (\lambda (_: nat).O) in (let
837 TMP_86 \def (lift_weight_add_O TMP_84 u O TMP_85) in (let TMP_87 \def (eq_ind
838 nat TMP_56 TMP_60 TMP_73 TMP_81 TMP_86) in (let TMP_88 \def (subst0_weight_lt
839 u t z O H TMP_42 TMP_47 TMP_53 TMP_87) in (let TMP_89 \def (le_lt_plus_plus
840 TMP_20 TMP_22 TMP_28 TMP_34 TMP_37 TMP_88) in (lt_n_S TMP_9 TMP_18
841 TMP_89))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
845 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
846 (THead (Bind Abbr) u t)))))
848 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
849 z)).(let TMP_1 \def (Bind Abbr) in (let TMP_2 \def (THead TMP_1 u z) in (let
850 TMP_3 \def (Bind Abbr) in (let TMP_4 \def (THead TMP_3 u t) in (let TMP_5
851 \def (Bind Abbr) in (let TMP_6 \def (tlt_head_dx TMP_5 u z) in (let TMP_7
852 \def (subst0_tlt_head u t z H) in (tlt_trans TMP_2 z TMP_4 TMP_6
projects / helm.git / blob