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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props".
19 include "tlt/defs.ma".
22 \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
23 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
24 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
26 \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
27 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
28 nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
29 nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
30 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
33 \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
34 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
35 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
37 \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
38 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
39 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
40 nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
41 (\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
45 \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
47 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
48 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
49 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
52 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
53 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
56 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
57 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
58 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
59 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall
60 (n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda
61 (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
62 (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k:
63 K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to
64 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
65 \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1:
66 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
67 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
68 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
69 (n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
70 (weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
71 B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
72 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
73 (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to
74 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
75 \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to
76 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
77 \to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
78 (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
79 (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
80 (weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
81 \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
82 t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
83 O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
84 t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
85 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
86 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
87 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
88 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
89 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
90 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
91 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
92 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
93 (plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
94 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
95 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
96 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
97 (le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
98 (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
99 ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
100 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
101 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
102 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
103 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
104 (f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
105 t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
106 (plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
107 t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map
108 (wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1))
109 (plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O)
110 t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda
111 (n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) (\lambda (t0:
112 T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
113 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
114 (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat
115 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g
116 n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
117 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
118 (f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
119 t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
120 (plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
121 t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map
122 (wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1))
123 (plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O)
124 t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda
125 (n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) b)) (\lambda (_:
126 F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to nat))).(\forall (g:
127 ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n)))) \to (le (weight_map
128 f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f0:
129 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n)
130 (g n)))) \to (le (weight_map f0 t1) (weight_map g t1))))))).(\lambda (f0:
131 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n:
132 nat).(le (f0 n) (g n))))).(lt_le_S (plus (weight_map f0 t0) (weight_map f0
133 t1)) (S (plus (weight_map g t0) (weight_map g t1))) (le_lt_n_Sm (plus
134 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
135 t1)) (plus_le_compat (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
136 (weight_map g t1) (H f0 g H1) (H0 f0 g H1)))))))))))) k)) t).
139 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
140 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
141 t) (weight_map g t)))))
143 \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
144 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
145 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
146 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
147 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
148 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
150 theorem weight_add_O:
151 \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
152 (weight_map (\lambda (_: nat).O) t))
154 \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
155 nat).O) (\lambda (n: nat).(wadd_O n))).
157 theorem weight_add_S:
158 \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
159 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
161 \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
162 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(le_S_n (wadd (\lambda
163 (_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (le_n_S (wadd (\lambda
164 (_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (wadd_le (\lambda (_:
165 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_O_n (S
169 \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
172 \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
173 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
174 (weight v) (weight t) H H0))))).
177 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
179 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
180 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
181 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
182 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
183 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
184 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
185 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
186 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
187 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
188 (u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S
189 (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_:
190 nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (le_n_S (S (weight_map
191 (\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u)
192 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
193 u))) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map
194 (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map
195 (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u)
196 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
197 u))) t))))))) (\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda
198 (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map
199 (wadd (\lambda (_: nat).O) O) t))) (le_n_S (S (weight_map (\lambda (_:
200 nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
201 (\lambda (_: nat).O) O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u)
202 (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_:
203 nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map
204 (wadd (\lambda (_: nat).O) O) t))))))) (\lambda (u: T).(\lambda (t:
205 T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map
206 (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))
207 (le_n_S (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda
208 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))) (le_n_S
209 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
210 (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda
211 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))))))) b))
212 (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map
213 (\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u)
214 (weight_map (\lambda (_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_:
215 nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda
216 (_: nat).O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus
217 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
218 (le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
219 nat).O) t)))))))) k).
222 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
224 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
225 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
226 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
227 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
228 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
229 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
230 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
231 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
232 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
233 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
234 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
235 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
236 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
237 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
238 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
239 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
240 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
241 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
242 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
243 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
244 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
245 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
246 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
247 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
248 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
249 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
250 (weight_map (\lambda (_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_:
251 nat).O) t)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda
252 (_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus
253 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
254 (le_n_S (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_:
255 nat).O) u) (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map
256 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))))) (weight_map
257 (wadd (\lambda (_: nat).O) O) t) (weight_add_O t)))) (\lambda (u: T).(\lambda
258 (t: T).(eq_ind_r nat (weight_map (\lambda (_: nat).O) t) (\lambda (n:
259 nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus (weight_map (\lambda
260 (_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
261 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
262 (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
263 (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
264 (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
265 (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u)
266 (weight_map (\lambda (_: nat).O) t))))) (weight_map (wadd (\lambda (_:
267 nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
268 T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
269 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
270 (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
271 (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
272 (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
273 (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u)
274 (weight_map (\lambda (_: nat).O) t)))))))) k).
276 theorem tlt_wf__q_ind:
277 \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
278 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
279 t))))) P n))) \to (\forall (t: T).(P t)))
281 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
282 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
283 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
284 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
288 \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
289 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
291 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
292 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
293 Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
294 (weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
295 (\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
296 T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
297 \to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
298 (weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall
299 (m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P
300 t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
301 (weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
302 v))))))))))))) t)))).