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/leq/asucc".
19 include "leq/props.ma".
21 include "aplus/props.ma".
24 \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (leq g
25 (asucc g a1) (asucc g a2)))))
27 \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
28 a2)).(leq_ind g (\lambda (a: A).(\lambda (a0: A).(leq g (asucc g a) (asucc g
29 a0)))) (\lambda (h1: nat).(\lambda (h2: nat).(\lambda (n1: nat).(\lambda (n2:
30 nat).(\lambda (k: nat).(\lambda (H0: (eq A (aplus g (ASort h1 n1) k) (aplus g
31 (ASort h2 n2) k))).((match h1 in nat return (\lambda (n: nat).((eq A (aplus g
32 (ASort n n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (match n with [O
33 \Rightarrow (ASort O (next g n1)) | (S h) \Rightarrow (ASort h n1)]) (match
34 h2 with [O \Rightarrow (ASort O (next g n2)) | (S h) \Rightarrow (ASort h
35 n2)])))) with [O \Rightarrow (\lambda (H1: (eq A (aplus g (ASort O n1) k)
36 (aplus g (ASort h2 n2) k))).((match h2 in nat return (\lambda (n: nat).((eq A
37 (aplus g (ASort O n1) k) (aplus g (ASort n n2) k)) \to (leq g (ASort O (next
38 g n1)) (match n with [O \Rightarrow (ASort O (next g n2)) | (S h) \Rightarrow
39 (ASort h n2)])))) with [O \Rightarrow (\lambda (H2: (eq A (aplus g (ASort O
40 n1) k) (aplus g (ASort O n2) k))).(leq_sort g O O (next g n1) (next g n2) k
41 (eq_ind A (aplus g (ASort O n1) (S k)) (\lambda (a: A).(eq A a (aplus g
42 (ASort O (next g n2)) k))) (eq_ind A (aplus g (ASort O n2) (S k)) (\lambda
43 (a: A).(eq A (aplus g (ASort O n1) (S k)) a)) (eq_ind_r A (aplus g (ASort O
44 n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc g (aplus g (ASort O n2) k))))
45 (refl_equal A (asucc g (aplus g (ASort O n2) k))) (aplus g (ASort O n1) k)
46 H2) (aplus g (ASort O (next g n2)) k) (aplus_sort_O_S_simpl g n2 k)) (aplus g
47 (ASort O (next g n1)) k) (aplus_sort_O_S_simpl g n1 k)))) | (S n) \Rightarrow
48 (\lambda (H2: (eq A (aplus g (ASort O n1) k) (aplus g (ASort (S n) n2)
49 k))).(leq_sort g O n (next g n1) n2 k (eq_ind A (aplus g (ASort O n1) (S k))
50 (\lambda (a: A).(eq A a (aplus g (ASort n n2) k))) (eq_ind A (aplus g (ASort
51 (S n) n2) (S k)) (\lambda (a: A).(eq A (aplus g (ASort O n1) (S k)) a))
52 (eq_ind_r A (aplus g (ASort (S n) n2) k) (\lambda (a: A).(eq A (asucc g a)
53 (asucc g (aplus g (ASort (S n) n2) k)))) (refl_equal A (asucc g (aplus g
54 (ASort (S n) n2) k))) (aplus g (ASort O n1) k) H2) (aplus g (ASort n n2) k)
55 (aplus_sort_S_S_simpl g n2 n k)) (aplus g (ASort O (next g n1)) k)
56 (aplus_sort_O_S_simpl g n1 k))))]) H1)) | (S n) \Rightarrow (\lambda (H1: (eq
57 A (aplus g (ASort (S n) n1) k) (aplus g (ASort h2 n2) k))).((match h2 in nat
58 return (\lambda (n0: nat).((eq A (aplus g (ASort (S n) n1) k) (aplus g (ASort
59 n0 n2) k)) \to (leq g (ASort n n1) (match n0 with [O \Rightarrow (ASort O
60 (next g n2)) | (S h) \Rightarrow (ASort h n2)])))) with [O \Rightarrow
61 (\lambda (H2: (eq A (aplus g (ASort (S n) n1) k) (aplus g (ASort O n2)
62 k))).(leq_sort g n O n1 (next g n2) k (eq_ind A (aplus g (ASort O n2) (S k))
63 (\lambda (a: A).(eq A (aplus g (ASort n n1) k) a)) (eq_ind A (aplus g (ASort
64 (S n) n1) (S k)) (\lambda (a: A).(eq A a (aplus g (ASort O n2) (S k))))
65 (eq_ind_r A (aplus g (ASort O n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc
66 g (aplus g (ASort O n2) k)))) (refl_equal A (asucc g (aplus g (ASort O n2)
67 k))) (aplus g (ASort (S n) n1) k) H2) (aplus g (ASort n n1) k)
68 (aplus_sort_S_S_simpl g n1 n k)) (aplus g (ASort O (next g n2)) k)
69 (aplus_sort_O_S_simpl g n2 k)))) | (S n0) \Rightarrow (\lambda (H2: (eq A
70 (aplus g (ASort (S n) n1) k) (aplus g (ASort (S n0) n2) k))).(leq_sort g n n0
71 n1 n2 k (eq_ind A (aplus g (ASort (S n) n1) (S k)) (\lambda (a: A).(eq A a
72 (aplus g (ASort n0 n2) k))) (eq_ind A (aplus g (ASort (S n0) n2) (S k))
73 (\lambda (a: A).(eq A (aplus g (ASort (S n) n1) (S k)) a)) (eq_ind_r A (aplus
74 g (ASort (S n0) n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc g (aplus g
75 (ASort (S n0) n2) k)))) (refl_equal A (asucc g (aplus g (ASort (S n0) n2)
76 k))) (aplus g (ASort (S n) n1) k) H2) (aplus g (ASort n0 n2) k)
77 (aplus_sort_S_S_simpl g n2 n0 k)) (aplus g (ASort n n1) k)
78 (aplus_sort_S_S_simpl g n1 n k))))]) H1))]) H0))))))) (\lambda (a3:
79 A).(\lambda (a4: A).(\lambda (H0: (leq g a3 a4)).(\lambda (_: (leq g (asucc g
80 a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_: (leq g a5
81 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g a3 a4 H0
82 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).
85 \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc
86 g a2)) \to (leq g a1 a2))))
88 \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2:
89 A).((leq g (asucc g a) (asucc g a2)) \to (leq g a a2)))) (\lambda (n:
90 nat).(\lambda (n0: nat).(\lambda (a2: A).(A_ind (\lambda (a: A).((leq g
91 (asucc g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a))) (\lambda
92 (n1: nat).(\lambda (n2: nat).(\lambda (H: (leq g (asucc g (ASort n n0))
93 (asucc g (ASort n1 n2)))).((match n in nat return (\lambda (n3: nat).((leq g
94 (asucc g (ASort n3 n0)) (asucc g (ASort n1 n2))) \to (leq g (ASort n3 n0)
95 (ASort n1 n2)))) with [O \Rightarrow (\lambda (H0: (leq g (asucc g (ASort O
96 n0)) (asucc g (ASort n1 n2)))).((match n1 in nat return (\lambda (n3:
97 nat).((leq g (asucc g (ASort O n0)) (asucc g (ASort n3 n2))) \to (leq g
98 (ASort O n0) (ASort n3 n2)))) with [O \Rightarrow (\lambda (H1: (leq g (asucc
99 g (ASort O n0)) (asucc g (ASort O n2)))).(let H2 \def (match H1 in leq return
100 (\lambda (a: A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort O
101 (next g n0))) \to ((eq A a0 (ASort O (next g n2))) \to (leq g (ASort O n0)
102 (ASort O n2))))))) with [(leq_sort h1 h2 n3 n4 k H2) \Rightarrow (\lambda
103 (H3: (eq A (ASort h1 n3) (ASort O (next g n0)))).(\lambda (H4: (eq A (ASort
104 h2 n4) (ASort O (next g n2)))).((let H5 \def (f_equal A nat (\lambda (e:
105 A).(match e in A return (\lambda (_: A).nat) with [(ASort _ n5) \Rightarrow
106 n5 | (AHead _ _) \Rightarrow n3])) (ASort h1 n3) (ASort O (next g n0)) H3) in
107 ((let H6 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda
108 (_: A).nat) with [(ASort n5 _) \Rightarrow n5 | (AHead _ _) \Rightarrow h1]))
109 (ASort h1 n3) (ASort O (next g n0)) H3) in (eq_ind nat O (\lambda (n5:
110 nat).((eq nat n3 (next g n0)) \to ((eq A (ASort h2 n4) (ASort O (next g n2)))
111 \to ((eq A (aplus g (ASort n5 n3) k) (aplus g (ASort h2 n4) k)) \to (leq g
112 (ASort O n0) (ASort O n2)))))) (\lambda (H7: (eq nat n3 (next g n0))).(eq_ind
113 nat (next g n0) (\lambda (n5: nat).((eq A (ASort h2 n4) (ASort O (next g
114 n2))) \to ((eq A (aplus g (ASort O n5) k) (aplus g (ASort h2 n4) k)) \to (leq
115 g (ASort O n0) (ASort O n2))))) (\lambda (H8: (eq A (ASort h2 n4) (ASort O
116 (next g n2)))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A
117 return (\lambda (_: A).nat) with [(ASort _ n5) \Rightarrow n5 | (AHead _ _)
118 \Rightarrow n4])) (ASort h2 n4) (ASort O (next g n2)) H8) in ((let H10 \def
119 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
120 [(ASort n5 _) \Rightarrow n5 | (AHead _ _) \Rightarrow h2])) (ASort h2 n4)
121 (ASort O (next g n2)) H8) in (eq_ind nat O (\lambda (n5: nat).((eq nat n4
122 (next g n2)) \to ((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort n5
123 n4) k)) \to (leq g (ASort O n0) (ASort O n2))))) (\lambda (H11: (eq nat n4
124 (next g n2))).(eq_ind nat (next g n2) (\lambda (n5: nat).((eq A (aplus g
125 (ASort O (next g n0)) k) (aplus g (ASort O n5) k)) \to (leq g (ASort O n0)
126 (ASort O n2)))) (\lambda (H12: (eq A (aplus g (ASort O (next g n0)) k) (aplus
127 g (ASort O (next g n2)) k))).(let H13 \def (eq_ind_r A (aplus g (ASort O
128 (next g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort O (next g n2)) k)))
129 H12 (aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let H14
130 \def (eq_ind_r A (aplus g (ASort O (next g n2)) k) (\lambda (a: A).(eq A
131 (aplus g (ASort O n0) (S k)) a)) H13 (aplus g (ASort O n2) (S k))
132 (aplus_sort_O_S_simpl g n2 k)) in (leq_sort g O O n0 n2 (S k) H14)))) n4
133 (sym_eq nat n4 (next g n2) H11))) h2 (sym_eq nat h2 O H10))) H9))) n3 (sym_eq
134 nat n3 (next g n0) H7))) h1 (sym_eq nat h1 O H6))) H5)) H4 H2))) | (leq_head
135 a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort O
136 (next g n0)))).(\lambda (H5: (eq A (AHead a3 a5) (ASort O (next g
137 n2)))).((let H6 \def (eq_ind A (AHead a0 a4) (\lambda (e: A).(match e in A
138 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
139 _) \Rightarrow True])) I (ASort O (next g n0)) H4) in (False_ind ((eq A
140 (AHead a3 a5) (ASort O (next g n2))) \to ((leq g a0 a3) \to ((leq g a4 a5)
141 \to (leq g (ASort O n0) (ASort O n2))))) H6)) H5 H2 H3)))]) in (H2
142 (refl_equal A (ASort O (next g n0))) (refl_equal A (ASort O (next g n2))))))
143 | (S n3) \Rightarrow (\lambda (H1: (leq g (asucc g (ASort O n0)) (asucc g
144 (ASort (S n3) n2)))).(let H2 \def (match H1 in leq return (\lambda (a:
145 A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort O (next g
146 n0))) \to ((eq A a0 (ASort n3 n2)) \to (leq g (ASort O n0) (ASort (S n3)
147 n2))))))) with [(leq_sort h1 h2 n4 n5 k H2) \Rightarrow (\lambda (H3: (eq A
148 (ASort h1 n4) (ASort O (next g n0)))).(\lambda (H4: (eq A (ASort h2 n5)
149 (ASort n3 n2))).((let H5 \def (f_equal A nat (\lambda (e: A).(match e in A
150 return (\lambda (_: A).nat) with [(ASort _ n6) \Rightarrow n6 | (AHead _ _)
151 \Rightarrow n4])) (ASort h1 n4) (ASort O (next g n0)) H3) in ((let H6 \def
152 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
153 [(ASort n6 _) \Rightarrow n6 | (AHead _ _) \Rightarrow h1])) (ASort h1 n4)
154 (ASort O (next g n0)) H3) in (eq_ind nat O (\lambda (n6: nat).((eq nat n4
155 (next g n0)) \to ((eq A (ASort h2 n5) (ASort n3 n2)) \to ((eq A (aplus g
156 (ASort n6 n4) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort O n0) (ASort (S
157 n3) n2)))))) (\lambda (H7: (eq nat n4 (next g n0))).(eq_ind nat (next g n0)
158 (\lambda (n6: nat).((eq A (ASort h2 n5) (ASort n3 n2)) \to ((eq A (aplus g
159 (ASort O n6) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort O n0) (ASort (S
160 n3) n2))))) (\lambda (H8: (eq A (ASort h2 n5) (ASort n3 n2))).(let H9 \def
161 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
162 [(ASort _ n6) \Rightarrow n6 | (AHead _ _) \Rightarrow n5])) (ASort h2 n5)
163 (ASort n3 n2) H8) in ((let H10 \def (f_equal A nat (\lambda (e: A).(match e
164 in A return (\lambda (_: A).nat) with [(ASort n6 _) \Rightarrow n6 | (AHead _
165 _) \Rightarrow h2])) (ASort h2 n5) (ASort n3 n2) H8) in (eq_ind nat n3
166 (\lambda (n6: nat).((eq nat n5 n2) \to ((eq A (aplus g (ASort O (next g n0))
167 k) (aplus g (ASort n6 n5) k)) \to (leq g (ASort O n0) (ASort (S n3) n2)))))
168 (\lambda (H11: (eq nat n5 n2)).(eq_ind nat n2 (\lambda (n6: nat).((eq A
169 (aplus g (ASort O (next g n0)) k) (aplus g (ASort n3 n6) k)) \to (leq g
170 (ASort O n0) (ASort (S n3) n2)))) (\lambda (H12: (eq A (aplus g (ASort O
171 (next g n0)) k) (aplus g (ASort n3 n2) k))).(let H13 \def (eq_ind_r A (aplus
172 g (ASort O (next g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort n3 n2)
173 k))) H12 (aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let
174 H14 \def (eq_ind_r A (aplus g (ASort n3 n2) k) (\lambda (a: A).(eq A (aplus g
175 (ASort O n0) (S k)) a)) H13 (aplus g (ASort (S n3) n2) (S k))
176 (aplus_sort_S_S_simpl g n2 n3 k)) in (leq_sort g O (S n3) n0 n2 (S k) H14))))
177 n5 (sym_eq nat n5 n2 H11))) h2 (sym_eq nat h2 n3 H10))) H9))) n4 (sym_eq nat
178 n4 (next g n0) H7))) h1 (sym_eq nat h1 O H6))) H5)) H4 H2))) | (leq_head a0
179 a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort O (next
180 g n0)))).(\lambda (H5: (eq A (AHead a3 a5) (ASort n3 n2))).((let H6 \def
181 (eq_ind A (AHead a0 a4) (\lambda (e: A).(match e in A return (\lambda (_:
182 A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
183 True])) I (ASort O (next g n0)) H4) in (False_ind ((eq A (AHead a3 a5) (ASort
184 n3 n2)) \to ((leq g a0 a3) \to ((leq g a4 a5) \to (leq g (ASort O n0) (ASort
185 (S n3) n2))))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (ASort O (next g n0)))
186 (refl_equal A (ASort n3 n2)))))]) H0)) | (S n3) \Rightarrow (\lambda (H0:
187 (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2)))).((match n1 in
188 nat return (\lambda (n4: nat).((leq g (asucc g (ASort (S n3) n0)) (asucc g
189 (ASort n4 n2))) \to (leq g (ASort (S n3) n0) (ASort n4 n2)))) with [O
190 \Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort
191 O n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda (a0:
192 A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0 (ASort O
193 (next g n2))) \to (leq g (ASort (S n3) n0) (ASort O n2))))))) with [(leq_sort
194 h1 h2 n4 n5 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n4) (ASort n3
195 n0))).(\lambda (H4: (eq A (ASort h2 n5) (ASort O (next g n2)))).((let H5 \def
196 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
197 [(ASort _ n6) \Rightarrow n6 | (AHead _ _) \Rightarrow n4])) (ASort h1 n4)
198 (ASort n3 n0) H3) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match e in
199 A return (\lambda (_: A).nat) with [(ASort n6 _) \Rightarrow n6 | (AHead _ _)
200 \Rightarrow h1])) (ASort h1 n4) (ASort n3 n0) H3) in (eq_ind nat n3 (\lambda
201 (n6: nat).((eq nat n4 n0) \to ((eq A (ASort h2 n5) (ASort O (next g n2))) \to
202 ((eq A (aplus g (ASort n6 n4) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort
203 (S n3) n0) (ASort O n2)))))) (\lambda (H7: (eq nat n4 n0)).(eq_ind nat n0
204 (\lambda (n6: nat).((eq A (ASort h2 n5) (ASort O (next g n2))) \to ((eq A
205 (aplus g (ASort n3 n6) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort (S n3)
206 n0) (ASort O n2))))) (\lambda (H8: (eq A (ASort h2 n5) (ASort O (next g
207 n2)))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A return
208 (\lambda (_: A).nat) with [(ASort _ n6) \Rightarrow n6 | (AHead _ _)
209 \Rightarrow n5])) (ASort h2 n5) (ASort O (next g n2)) H8) in ((let H10 \def
210 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
211 [(ASort n6 _) \Rightarrow n6 | (AHead _ _) \Rightarrow h2])) (ASort h2 n5)
212 (ASort O (next g n2)) H8) in (eq_ind nat O (\lambda (n6: nat).((eq nat n5
213 (next g n2)) \to ((eq A (aplus g (ASort n3 n0) k) (aplus g (ASort n6 n5) k))
214 \to (leq g (ASort (S n3) n0) (ASort O n2))))) (\lambda (H11: (eq nat n5 (next
215 g n2))).(eq_ind nat (next g n2) (\lambda (n6: nat).((eq A (aplus g (ASort n3
216 n0) k) (aplus g (ASort O n6) k)) \to (leq g (ASort (S n3) n0) (ASort O n2))))
217 (\lambda (H12: (eq A (aplus g (ASort n3 n0) k) (aplus g (ASort O (next g n2))
218 k))).(let H13 \def (eq_ind_r A (aplus g (ASort n3 n0) k) (\lambda (a: A).(eq
219 A a (aplus g (ASort O (next g n2)) k))) H12 (aplus g (ASort (S n3) n0) (S k))
220 (aplus_sort_S_S_simpl g n0 n3 k)) in (let H14 \def (eq_ind_r A (aplus g
221 (ASort O (next g n2)) k) (\lambda (a: A).(eq A (aplus g (ASort (S n3) n0) (S
222 k)) a)) H13 (aplus g (ASort O n2) (S k)) (aplus_sort_O_S_simpl g n2 k)) in
223 (leq_sort g (S n3) O n0 n2 (S k) H14)))) n5 (sym_eq nat n5 (next g n2) H11)))
224 h2 (sym_eq nat h2 O H10))) H9))) n4 (sym_eq nat n4 n0 H7))) h1 (sym_eq nat h1
225 n3 H6))) H5)) H4 H2))) | (leq_head a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda
226 (H4: (eq A (AHead a0 a4) (ASort n3 n0))).(\lambda (H5: (eq A (AHead a3 a5)
227 (ASort O (next g n2)))).((let H6 \def (eq_ind A (AHead a0 a4) (\lambda (e:
228 A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow
229 False | (AHead _ _) \Rightarrow True])) I (ASort n3 n0) H4) in (False_ind
230 ((eq A (AHead a3 a5) (ASort O (next g n2))) \to ((leq g a0 a3) \to ((leq g a4
231 a5) \to (leq g (ASort (S n3) n0) (ASort O n2))))) H6)) H5 H2 H3)))]) in (H2
232 (refl_equal A (ASort n3 n0)) (refl_equal A (ASort O (next g n2)))))) | (S n4)
233 \Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort
234 (S n4) n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda
235 (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0
236 (ASort n4 n2)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2))))))) with
237 [(leq_sort h1 h2 n5 n6 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n5)
238 (ASort n3 n0))).(\lambda (H4: (eq A (ASort h2 n6) (ASort n4 n2))).((let H5
239 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat)
240 with [(ASort _ n7) \Rightarrow n7 | (AHead _ _) \Rightarrow n5])) (ASort h1
241 n5) (ASort n3 n0) H3) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match
242 e in A return (\lambda (_: A).nat) with [(ASort n7 _) \Rightarrow n7 | (AHead
243 _ _) \Rightarrow h1])) (ASort h1 n5) (ASort n3 n0) H3) in (eq_ind nat n3
244 (\lambda (n7: nat).((eq nat n5 n0) \to ((eq A (ASort h2 n6) (ASort n4 n2))
245 \to ((eq A (aplus g (ASort n7 n5) k) (aplus g (ASort h2 n6) k)) \to (leq g
246 (ASort (S n3) n0) (ASort (S n4) n2)))))) (\lambda (H7: (eq nat n5
247 n0)).(eq_ind nat n0 (\lambda (n7: nat).((eq A (ASort h2 n6) (ASort n4 n2))
248 \to ((eq A (aplus g (ASort n3 n7) k) (aplus g (ASort h2 n6) k)) \to (leq g
249 (ASort (S n3) n0) (ASort (S n4) n2))))) (\lambda (H8: (eq A (ASort h2 n6)
250 (ASort n4 n2))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A
251 return (\lambda (_: A).nat) with [(ASort _ n7) \Rightarrow n7 | (AHead _ _)
252 \Rightarrow n6])) (ASort h2 n6) (ASort n4 n2) H8) in ((let H10 \def (f_equal
253 A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with [(ASort
254 n7 _) \Rightarrow n7 | (AHead _ _) \Rightarrow h2])) (ASort h2 n6) (ASort n4
255 n2) H8) in (eq_ind nat n4 (\lambda (n7: nat).((eq nat n6 n2) \to ((eq A
256 (aplus g (ASort n3 n0) k) (aplus g (ASort n7 n6) k)) \to (leq g (ASort (S n3)
257 n0) (ASort (S n4) n2))))) (\lambda (H11: (eq nat n6 n2)).(eq_ind nat n2
258 (\lambda (n7: nat).((eq A (aplus g (ASort n3 n0) k) (aplus g (ASort n4 n7)
259 k)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2)))) (\lambda (H12: (eq A
260 (aplus g (ASort n3 n0) k) (aplus g (ASort n4 n2) k))).(let H13 \def (eq_ind_r
261 A (aplus g (ASort n3 n0) k) (\lambda (a: A).(eq A a (aplus g (ASort n4 n2)
262 k))) H12 (aplus g (ASort (S n3) n0) (S k)) (aplus_sort_S_S_simpl g n0 n3 k))
263 in (let H14 \def (eq_ind_r A (aplus g (ASort n4 n2) k) (\lambda (a: A).(eq A
264 (aplus g (ASort (S n3) n0) (S k)) a)) H13 (aplus g (ASort (S n4) n2) (S k))
265 (aplus_sort_S_S_simpl g n2 n4 k)) in (leq_sort g (S n3) (S n4) n0 n2 (S k)
266 H14)))) n6 (sym_eq nat n6 n2 H11))) h2 (sym_eq nat h2 n4 H10))) H9))) n5
267 (sym_eq nat n5 n0 H7))) h1 (sym_eq nat h1 n3 H6))) H5)) H4 H2))) | (leq_head
268 a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort n3
269 n0))).(\lambda (H5: (eq A (AHead a3 a5) (ASort n4 n2))).((let H6 \def (eq_ind
270 A (AHead a0 a4) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop)
271 with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow True])) I
272 (ASort n3 n0) H4) in (False_ind ((eq A (AHead a3 a5) (ASort n4 n2)) \to ((leq
273 g a0 a3) \to ((leq g a4 a5) \to (leq g (ASort (S n3) n0) (ASort (S n4)
274 n2))))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (ASort n3 n0)) (refl_equal A
275 (ASort n4 n2)))))]) H0))]) H)))) (\lambda (a: A).(\lambda (H: (((leq g (asucc
276 g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a)))).(\lambda (a0:
277 A).(\lambda (H0: (((leq g (asucc g (ASort n n0)) (asucc g a0)) \to (leq g
278 (ASort n n0) a0)))).(\lambda (H1: (leq g (asucc g (ASort n n0)) (asucc g
279 (AHead a a0)))).((match n in nat return (\lambda (n1: nat).((((leq g (asucc g
280 (ASort n1 n0)) (asucc g a)) \to (leq g (ASort n1 n0) a))) \to ((((leq g
281 (asucc g (ASort n1 n0)) (asucc g a0)) \to (leq g (ASort n1 n0) a0))) \to
282 ((leq g (asucc g (ASort n1 n0)) (asucc g (AHead a a0))) \to (leq g (ASort n1
283 n0) (AHead a a0)))))) with [O \Rightarrow (\lambda (_: (((leq g (asucc g
284 (ASort O n0)) (asucc g a)) \to (leq g (ASort O n0) a)))).(\lambda (_: (((leq
285 g (asucc g (ASort O n0)) (asucc g a0)) \to (leq g (ASort O n0)
286 a0)))).(\lambda (H4: (leq g (asucc g (ASort O n0)) (asucc g (AHead a
287 a0)))).(let H5 \def (match H4 in leq return (\lambda (a3: A).(\lambda (a4:
288 A).(\lambda (_: (leq ? a3 a4)).((eq A a3 (ASort O (next g n0))) \to ((eq A a4
289 (AHead a (asucc g a0))) \to (leq g (ASort O n0) (AHead a a0))))))) with
290 [(leq_sort h1 h2 n1 n2 k H5) \Rightarrow (\lambda (H6: (eq A (ASort h1 n1)
291 (ASort O (next g n0)))).(\lambda (H7: (eq A (ASort h2 n2) (AHead a (asucc g
292 a0)))).((let H8 \def (f_equal A nat (\lambda (e: A).(match e in A return
293 (\lambda (_: A).nat) with [(ASort _ n3) \Rightarrow n3 | (AHead _ _)
294 \Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H6) in ((let H9 \def
295 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
296 [(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow h1])) (ASort h1 n1)
297 (ASort O (next g n0)) H6) in (eq_ind nat O (\lambda (n3: nat).((eq nat n1
298 (next g n0)) \to ((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A
299 (aplus g (ASort n3 n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0)
300 (AHead a a0)))))) (\lambda (H10: (eq nat n1 (next g n0))).(eq_ind nat (next g
301 n0) (\lambda (n3: nat).((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq
302 A (aplus g (ASort O n3) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0)
303 (AHead a a0))))) (\lambda (H11: (eq A (ASort h2 n2) (AHead a (asucc g
304 a0)))).(let H12 \def (eq_ind A (ASort h2 n2) (\lambda (e: A).(match e in A
305 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _)
306 \Rightarrow False])) I (AHead a (asucc g a0)) H11) in (False_ind ((eq A
307 (aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)) \to (leq g
308 (ASort O n0) (AHead a a0))) H12))) n1 (sym_eq nat n1 (next g n0) H10))) h1
309 (sym_eq nat h1 O H9))) H8)) H7 H5))) | (leq_head a3 a4 H5 a5 a6 H6)
310 \Rightarrow (\lambda (H7: (eq A (AHead a3 a5) (ASort O (next g
311 n0)))).(\lambda (H8: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).((let H9
312 \def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A return (\lambda
313 (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
314 True])) I (ASort O (next g n0)) H7) in (False_ind ((eq A (AHead a4 a6) (AHead
315 a (asucc g a0))) \to ((leq g a3 a4) \to ((leq g a5 a6) \to (leq g (ASort O
316 n0) (AHead a a0))))) H9)) H8 H5 H6)))]) in (H5 (refl_equal A (ASort O (next g
317 n0))) (refl_equal A (AHead a (asucc g a0)))))))) | (S n1) \Rightarrow
318 (\lambda (_: (((leq g (asucc g (ASort (S n1) n0)) (asucc g a)) \to (leq g
319 (ASort (S n1) n0) a)))).(\lambda (_: (((leq g (asucc g (ASort (S n1) n0))
320 (asucc g a0)) \to (leq g (ASort (S n1) n0) a0)))).(\lambda (H4: (leq g (asucc
321 g (ASort (S n1) n0)) (asucc g (AHead a a0)))).(let H5 \def (match H4 in leq
322 return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A
323 a3 (ASort n1 n0)) \to ((eq A a4 (AHead a (asucc g a0))) \to (leq g (ASort (S
324 n1) n0) (AHead a a0))))))) with [(leq_sort h1 h2 n2 n3 k H5) \Rightarrow
325 (\lambda (H6: (eq A (ASort h1 n2) (ASort n1 n0))).(\lambda (H7: (eq A (ASort
326 h2 n3) (AHead a (asucc g a0)))).((let H8 \def (f_equal A nat (\lambda (e:
327 A).(match e in A return (\lambda (_: A).nat) with [(ASort _ n4) \Rightarrow
328 n4 | (AHead _ _) \Rightarrow n2])) (ASort h1 n2) (ASort n1 n0) H6) in ((let
329 H9 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_:
330 A).nat) with [(ASort n4 _) \Rightarrow n4 | (AHead _ _) \Rightarrow h1]))
331 (ASort h1 n2) (ASort n1 n0) H6) in (eq_ind nat n1 (\lambda (n4: nat).((eq nat
332 n2 n0) \to ((eq A (ASort h2 n3) (AHead a (asucc g a0))) \to ((eq A (aplus g
333 (ASort n4 n2) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0)
334 (AHead a a0)))))) (\lambda (H10: (eq nat n2 n0)).(eq_ind nat n0 (\lambda (n4:
335 nat).((eq A (ASort h2 n3) (AHead a (asucc g a0))) \to ((eq A (aplus g (ASort
336 n1 n4) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0) (AHead a
337 a0))))) (\lambda (H11: (eq A (ASort h2 n3) (AHead a (asucc g a0)))).(let H12
338 \def (eq_ind A (ASort h2 n3) (\lambda (e: A).(match e in A return (\lambda
339 (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow
340 False])) I (AHead a (asucc g a0)) H11) in (False_ind ((eq A (aplus g (ASort
341 n1 n0) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0) (AHead a
342 a0))) H12))) n2 (sym_eq nat n2 n0 H10))) h1 (sym_eq nat h1 n1 H9))) H8)) H7
343 H5))) | (leq_head a3 a4 H5 a5 a6 H6) \Rightarrow (\lambda (H7: (eq A (AHead
344 a3 a5) (ASort n1 n0))).(\lambda (H8: (eq A (AHead a4 a6) (AHead a (asucc g
345 a0)))).((let H9 \def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A
346 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
347 _) \Rightarrow True])) I (ASort n1 n0) H7) in (False_ind ((eq A (AHead a4 a6)
348 (AHead a (asucc g a0))) \to ((leq g a3 a4) \to ((leq g a5 a6) \to (leq g
349 (ASort (S n1) n0) (AHead a a0))))) H9)) H8 H5 H6)))]) in (H5 (refl_equal A
350 (ASort n1 n0)) (refl_equal A (AHead a (asucc g a0))))))))]) H H0 H1))))))
351 a2)))) (\lambda (a: A).(\lambda (_: ((\forall (a2: A).((leq g (asucc g a)
352 (asucc g a2)) \to (leq g a a2))))).(\lambda (a0: A).(\lambda (H0: ((\forall
353 (a2: A).((leq g (asucc g a0) (asucc g a2)) \to (leq g a0 a2))))).(\lambda
354 (a2: A).(A_ind (\lambda (a3: A).((leq g (asucc g (AHead a a0)) (asucc g a3))
355 \to (leq g (AHead a a0) a3))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda
356 (H1: (leq g (asucc g (AHead a a0)) (asucc g (ASort n n0)))).((match n in nat
357 return (\lambda (n1: nat).((leq g (asucc g (AHead a a0)) (asucc g (ASort n1
358 n0))) \to (leq g (AHead a a0) (ASort n1 n0)))) with [O \Rightarrow (\lambda
359 (H2: (leq g (asucc g (AHead a a0)) (asucc g (ASort O n0)))).(let H3 \def
360 (match H2 in leq return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ?
361 a3 a4)).((eq A a3 (AHead a (asucc g a0))) \to ((eq A a4 (ASort O (next g
362 n0))) \to (leq g (AHead a a0) (ASort O n0))))))) with [(leq_sort h1 h2 n1 n2
363 k H3) \Rightarrow (\lambda (H4: (eq A (ASort h1 n1) (AHead a (asucc g
364 a0)))).(\lambda (H5: (eq A (ASort h2 n2) (ASort O (next g n0)))).((let H6
365 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda
366 (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow
367 False])) I (AHead a (asucc g a0)) H4) in (False_ind ((eq A (ASort h2 n2)
368 (ASort O (next g n0))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort
369 h2 n2) k)) \to (leq g (AHead a a0) (ASort O n0)))) H6)) H5 H3))) | (leq_head
370 a3 a4 H3 a5 a6 H4) \Rightarrow (\lambda (H5: (eq A (AHead a3 a5) (AHead a
371 (asucc g a0)))).(\lambda (H6: (eq A (AHead a4 a6) (ASort O (next g
372 n0)))).((let H7 \def (f_equal A A (\lambda (e: A).(match e in A return
373 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a5 | (AHead _ a7)
374 \Rightarrow a7])) (AHead a3 a5) (AHead a (asucc g a0)) H5) in ((let H8 \def
375 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
376 [(ASort _ _) \Rightarrow a3 | (AHead a7 _) \Rightarrow a7])) (AHead a3 a5)
377 (AHead a (asucc g a0)) H5) in (eq_ind A a (\lambda (a7: A).((eq A a5 (asucc g
378 a0)) \to ((eq A (AHead a4 a6) (ASort O (next g n0))) \to ((leq g a7 a4) \to
379 ((leq g a5 a6) \to (leq g (AHead a a0) (ASort O n0))))))) (\lambda (H9: (eq A
380 a5 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((eq A (AHead a4
381 a6) (ASort O (next g n0))) \to ((leq g a a4) \to ((leq g a7 a6) \to (leq g
382 (AHead a a0) (ASort O n0)))))) (\lambda (H10: (eq A (AHead a4 a6) (ASort O
383 (next g n0)))).(let H11 \def (eq_ind A (AHead a4 a6) (\lambda (e: A).(match e
384 in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False |
385 (AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H10) in (False_ind
386 ((leq g a a4) \to ((leq g (asucc g a0) a6) \to (leq g (AHead a a0) (ASort O
387 n0)))) H11))) a5 (sym_eq A a5 (asucc g a0) H9))) a3 (sym_eq A a3 a H8))) H7))
388 H6 H3 H4)))]) in (H3 (refl_equal A (AHead a (asucc g a0))) (refl_equal A
389 (ASort O (next g n0)))))) | (S n1) \Rightarrow (\lambda (H2: (leq g (asucc g
390 (AHead a a0)) (asucc g (ASort (S n1) n0)))).(let H3 \def (match H2 in leq
391 return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A
392 a3 (AHead a (asucc g a0))) \to ((eq A a4 (ASort n1 n0)) \to (leq g (AHead a
393 a0) (ASort (S n1) n0))))))) with [(leq_sort h1 h2 n2 n3 k H3) \Rightarrow
394 (\lambda (H4: (eq A (ASort h1 n2) (AHead a (asucc g a0)))).(\lambda (H5: (eq
395 A (ASort h2 n3) (ASort n1 n0))).((let H6 \def (eq_ind A (ASort h1 n2)
396 (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _)
397 \Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead a (asucc g a0))
398 H4) in (False_ind ((eq A (ASort h2 n3) (ASort n1 n0)) \to ((eq A (aplus g
399 (ASort h1 n2) k) (aplus g (ASort h2 n3) k)) \to (leq g (AHead a a0) (ASort (S
400 n1) n0)))) H6)) H5 H3))) | (leq_head a3 a4 H3 a5 a6 H4) \Rightarrow (\lambda
401 (H5: (eq A (AHead a3 a5) (AHead a (asucc g a0)))).(\lambda (H6: (eq A (AHead
402 a4 a6) (ASort n1 n0))).((let H7 \def (f_equal A A (\lambda (e: A).(match e in
403 A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a5 | (AHead _ a7)
404 \Rightarrow a7])) (AHead a3 a5) (AHead a (asucc g a0)) H5) in ((let H8 \def
405 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
406 [(ASort _ _) \Rightarrow a3 | (AHead a7 _) \Rightarrow a7])) (AHead a3 a5)
407 (AHead a (asucc g a0)) H5) in (eq_ind A a (\lambda (a7: A).((eq A a5 (asucc g
408 a0)) \to ((eq A (AHead a4 a6) (ASort n1 n0)) \to ((leq g a7 a4) \to ((leq g
409 a5 a6) \to (leq g (AHead a a0) (ASort (S n1) n0))))))) (\lambda (H9: (eq A a5
410 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((eq A (AHead a4 a6)
411 (ASort n1 n0)) \to ((leq g a a4) \to ((leq g a7 a6) \to (leq g (AHead a a0)
412 (ASort (S n1) n0)))))) (\lambda (H10: (eq A (AHead a4 a6) (ASort n1
413 n0))).(let H11 \def (eq_ind A (AHead a4 a6) (\lambda (e: A).(match e in A
414 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
415 _) \Rightarrow True])) I (ASort n1 n0) H10) in (False_ind ((leq g a a4) \to
416 ((leq g (asucc g a0) a6) \to (leq g (AHead a a0) (ASort (S n1) n0)))) H11)))
417 a5 (sym_eq A a5 (asucc g a0) H9))) a3 (sym_eq A a3 a H8))) H7)) H6 H3 H4)))])
418 in (H3 (refl_equal A (AHead a (asucc g a0))) (refl_equal A (ASort n1
419 n0)))))]) H1)))) (\lambda (a3: A).(\lambda (_: (((leq g (asucc g (AHead a
420 a0)) (asucc g a3)) \to (leq g (AHead a a0) a3)))).(\lambda (a4: A).(\lambda
421 (_: (((leq g (asucc g (AHead a a0)) (asucc g a4)) \to (leq g (AHead a a0)
422 a4)))).(\lambda (H3: (leq g (asucc g (AHead a a0)) (asucc g (AHead a3
423 a4)))).(let H4 \def (match H3 in leq return (\lambda (a5: A).(\lambda (a6:
424 A).(\lambda (_: (leq ? a5 a6)).((eq A a5 (AHead a (asucc g a0))) \to ((eq A
425 a6 (AHead a3 (asucc g a4))) \to (leq g (AHead a a0) (AHead a3 a4))))))) with
426 [(leq_sort h1 h2 n1 n2 k H4) \Rightarrow (\lambda (H5: (eq A (ASort h1 n1)
427 (AHead a (asucc g a0)))).(\lambda (H6: (eq A (ASort h2 n2) (AHead a3 (asucc g
428 a4)))).((let H7 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A
429 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _)
430 \Rightarrow False])) I (AHead a (asucc g a0)) H5) in (False_ind ((eq A (ASort
431 h2 n2) (AHead a3 (asucc g a4))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g
432 (ASort h2 n2) k)) \to (leq g (AHead a a0) (AHead a3 a4)))) H7)) H6 H4))) |
433 (leq_head a5 a6 H4 a7 a8 H5) \Rightarrow (\lambda (H6: (eq A (AHead a5 a7)
434 (AHead a (asucc g a0)))).(\lambda (H7: (eq A (AHead a6 a8) (AHead a3 (asucc g
435 a4)))).((let H8 \def (f_equal A A (\lambda (e: A).(match e in A return
436 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a7 | (AHead _ a9)
437 \Rightarrow a9])) (AHead a5 a7) (AHead a (asucc g a0)) H6) in ((let H9 \def
438 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
439 [(ASort _ _) \Rightarrow a5 | (AHead a9 _) \Rightarrow a9])) (AHead a5 a7)
440 (AHead a (asucc g a0)) H6) in (eq_ind A a (\lambda (a9: A).((eq A a7 (asucc g
441 a0)) \to ((eq A (AHead a6 a8) (AHead a3 (asucc g a4))) \to ((leq g a9 a6) \to
442 ((leq g a7 a8) \to (leq g (AHead a a0) (AHead a3 a4))))))) (\lambda (H10: (eq
443 A a7 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a9: A).((eq A (AHead a6
444 a8) (AHead a3 (asucc g a4))) \to ((leq g a a6) \to ((leq g a9 a8) \to (leq g
445 (AHead a a0) (AHead a3 a4)))))) (\lambda (H11: (eq A (AHead a6 a8) (AHead a3
446 (asucc g a4)))).(let H12 \def (f_equal A A (\lambda (e: A).(match e in A
447 return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a8 | (AHead _ a9)
448 \Rightarrow a9])) (AHead a6 a8) (AHead a3 (asucc g a4)) H11) in ((let H13
449 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
450 with [(ASort _ _) \Rightarrow a6 | (AHead a9 _) \Rightarrow a9])) (AHead a6
451 a8) (AHead a3 (asucc g a4)) H11) in (eq_ind A a3 (\lambda (a9: A).((eq A a8
452 (asucc g a4)) \to ((leq g a a9) \to ((leq g (asucc g a0) a8) \to (leq g
453 (AHead a a0) (AHead a3 a4)))))) (\lambda (H14: (eq A a8 (asucc g
454 a4))).(eq_ind A (asucc g a4) (\lambda (a9: A).((leq g a a3) \to ((leq g
455 (asucc g a0) a9) \to (leq g (AHead a a0) (AHead a3 a4))))) (\lambda (H15:
456 (leq g a a3)).(\lambda (H16: (leq g (asucc g a0) (asucc g a4))).(leq_head g a
457 a3 H15 a0 a4 (H0 a4 H16)))) a8 (sym_eq A a8 (asucc g a4) H14))) a6 (sym_eq A
458 a6 a3 H13))) H12))) a7 (sym_eq A a7 (asucc g a0) H10))) a5 (sym_eq A a5 a
459 H9))) H8)) H7 H4 H5)))]) in (H4 (refl_equal A (AHead a (asucc g a0)))
460 (refl_equal A (AHead a3 (asucc g a4)))))))))) a2)))))) a1)).
463 \forall (g: G).(\forall (a: A).(ex A (\lambda (a0: A).(leq g a (asucc g
466 \lambda (g: G).(\lambda (a: A).(A_ind (\lambda (a0: A).(ex A (\lambda (a1:
467 A).(leq g a0 (asucc g a1))))) (\lambda (n: nat).(\lambda (n0: nat).(ex_intro
468 A (\lambda (a0: A).(leq g (ASort n n0) (asucc g a0))) (ASort (S n) n0)
469 (leq_refl g (ASort n n0))))) (\lambda (a0: A).(\lambda (_: (ex A (\lambda
470 (a1: A).(leq g a0 (asucc g a1))))).(\lambda (a1: A).(\lambda (H0: (ex A
471 (\lambda (a2: A).(leq g a1 (asucc g a2))))).(let H1 \def H0 in (ex_ind A
472 (\lambda (a2: A).(leq g a1 (asucc g a2))) (ex A (\lambda (a2: A).(leq g
473 (AHead a0 a1) (asucc g a2)))) (\lambda (x: A).(\lambda (H2: (leq g a1 (asucc
474 g x))).(ex_intro A (\lambda (a2: A).(leq g (AHead a0 a1) (asucc g a2)))
475 (AHead a0 x) (leq_head g a0 a0 (leq_refl g a0) a1 (asucc g x) H2)))) H1))))))
478 theorem leq_ahead_asucc_false:
479 \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (AHead a1 a2)
480 (asucc g a1)) \to (\forall (P: Prop).P))))
482 \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2:
483 A).((leq g (AHead a a2) (asucc g a)) \to (\forall (P: Prop).P)))) (\lambda
484 (n: nat).(\lambda (n0: nat).(\lambda (a2: A).(\lambda (H: (leq g (AHead
485 (ASort n n0) a2) (match n with [O \Rightarrow (ASort O (next g n0)) | (S h)
486 \Rightarrow (ASort h n0)]))).(\lambda (P: Prop).((match n in nat return
487 (\lambda (n1: nat).((leq g (AHead (ASort n1 n0) a2) (match n1 with [O
488 \Rightarrow (ASort O (next g n0)) | (S h) \Rightarrow (ASort h n0)])) \to P))
489 with [O \Rightarrow (\lambda (H0: (leq g (AHead (ASort O n0) a2) (ASort O
490 (next g n0)))).(let H1 \def (match H0 in leq return (\lambda (a: A).(\lambda
491 (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (AHead (ASort O n0) a2)) \to ((eq
492 A a0 (ASort O (next g n0))) \to P))))) with [(leq_sort h1 h2 n1 n2 k H1)
493 \Rightarrow (\lambda (H2: (eq A (ASort h1 n1) (AHead (ASort O n0)
494 a2))).(\lambda (H3: (eq A (ASort h2 n2) (ASort O (next g n0)))).((let H4 \def
495 (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda (_:
496 A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow
497 False])) I (AHead (ASort O n0) a2) H2) in (False_ind ((eq A (ASort h2 n2)
498 (ASort O (next g n0))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort
499 h2 n2) k)) \to P)) H4)) H3 H1))) | (leq_head a0 a3 H1 a4 a5 H2) \Rightarrow
500 (\lambda (H3: (eq A (AHead a0 a4) (AHead (ASort O n0) a2))).(\lambda (H4: (eq
501 A (AHead a3 a5) (ASort O (next g n0)))).((let H5 \def (f_equal A A (\lambda
502 (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow
503 a4 | (AHead _ a) \Rightarrow a])) (AHead a0 a4) (AHead (ASort O n0) a2) H3)
504 in ((let H6 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda
505 (_: A).A) with [(ASort _ _) \Rightarrow a0 | (AHead a _) \Rightarrow a]))
506 (AHead a0 a4) (AHead (ASort O n0) a2) H3) in (eq_ind A (ASort O n0) (\lambda
507 (a: A).((eq A a4 a2) \to ((eq A (AHead a3 a5) (ASort O (next g n0))) \to
508 ((leq g a a3) \to ((leq g a4 a5) \to P))))) (\lambda (H7: (eq A a4
509 a2)).(eq_ind A a2 (\lambda (a: A).((eq A (AHead a3 a5) (ASort O (next g n0)))
510 \to ((leq g (ASort O n0) a3) \to ((leq g a a5) \to P)))) (\lambda (H8: (eq A
511 (AHead a3 a5) (ASort O (next g n0)))).(let H9 \def (eq_ind A (AHead a3 a5)
512 (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _)
513 \Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort O (next g n0))
514 H8) in (False_ind ((leq g (ASort O n0) a3) \to ((leq g a2 a5) \to P)) H9)))
515 a4 (sym_eq A a4 a2 H7))) a0 (sym_eq A a0 (ASort O n0) H6))) H5)) H4 H1
516 H2)))]) in (H1 (refl_equal A (AHead (ASort O n0) a2)) (refl_equal A (ASort O
517 (next g n0)))))) | (S n1) \Rightarrow (\lambda (H0: (leq g (AHead (ASort (S
518 n1) n0) a2) (ASort n1 n0))).(let H1 \def (match H0 in leq return (\lambda (a:
519 A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (AHead (ASort (S n1)
520 n0) a2)) \to ((eq A a0 (ASort n1 n0)) \to P))))) with [(leq_sort h1 h2 n2 n3
521 k H1) \Rightarrow (\lambda (H2: (eq A (ASort h1 n2) (AHead (ASort (S n1) n0)
522 a2))).(\lambda (H3: (eq A (ASort h2 n3) (ASort n1 n0))).((let H4 \def (eq_ind
523 A (ASort h1 n2) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop)
524 with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow False])) I
525 (AHead (ASort (S n1) n0) a2) H2) in (False_ind ((eq A (ASort h2 n3) (ASort n1
526 n0)) \to ((eq A (aplus g (ASort h1 n2) k) (aplus g (ASort h2 n3) k)) \to P))
527 H4)) H3 H1))) | (leq_head a0 a3 H1 a4 a5 H2) \Rightarrow (\lambda (H3: (eq A
528 (AHead a0 a4) (AHead (ASort (S n1) n0) a2))).(\lambda (H4: (eq A (AHead a3
529 a5) (ASort n1 n0))).((let H5 \def (f_equal A A (\lambda (e: A).(match e in A
530 return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead _ a)
531 \Rightarrow a])) (AHead a0 a4) (AHead (ASort (S n1) n0) a2) H3) in ((let H6
532 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
533 with [(ASort _ _) \Rightarrow a0 | (AHead a _) \Rightarrow a])) (AHead a0 a4)
534 (AHead (ASort (S n1) n0) a2) H3) in (eq_ind A (ASort (S n1) n0) (\lambda (a:
535 A).((eq A a4 a2) \to ((eq A (AHead a3 a5) (ASort n1 n0)) \to ((leq g a a3)
536 \to ((leq g a4 a5) \to P))))) (\lambda (H7: (eq A a4 a2)).(eq_ind A a2
537 (\lambda (a: A).((eq A (AHead a3 a5) (ASort n1 n0)) \to ((leq g (ASort (S n1)
538 n0) a3) \to ((leq g a a5) \to P)))) (\lambda (H8: (eq A (AHead a3 a5) (ASort
539 n1 n0))).(let H9 \def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A
540 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
541 _) \Rightarrow True])) I (ASort n1 n0) H8) in (False_ind ((leq g (ASort (S
542 n1) n0) a3) \to ((leq g a2 a5) \to P)) H9))) a4 (sym_eq A a4 a2 H7))) a0
543 (sym_eq A a0 (ASort (S n1) n0) H6))) H5)) H4 H1 H2)))]) in (H1 (refl_equal A
544 (AHead (ASort (S n1) n0) a2)) (refl_equal A (ASort n1 n0)))))]) H))))))
545 (\lambda (a: A).(\lambda (_: ((\forall (a2: A).((leq g (AHead a a2) (asucc g
546 a)) \to (\forall (P: Prop).P))))).(\lambda (a0: A).(\lambda (_: ((\forall
547 (a2: A).((leq g (AHead a0 a2) (asucc g a0)) \to (\forall (P:
548 Prop).P))))).(\lambda (a2: A).(\lambda (H1: (leq g (AHead (AHead a a0) a2)
549 (AHead a (asucc g a0)))).(\lambda (P: Prop).(let H2 \def (match H1 in leq
550 return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A
551 a3 (AHead (AHead a a0) a2)) \to ((eq A a4 (AHead a (asucc g a0))) \to P)))))
552 with [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1
553 n1) (AHead (AHead a a0) a2))).(\lambda (H4: (eq A (ASort h2 n2) (AHead a
554 (asucc g a0)))).((let H5 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match
555 e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True |
556 (AHead _ _) \Rightarrow False])) I (AHead (AHead a a0) a2) H3) in (False_ind
557 ((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A (aplus g (ASort h1
558 n1) k) (aplus g (ASort h2 n2) k)) \to P)) H5)) H4 H2))) | (leq_head a3 a4 H2
559 a5 a6 H3) \Rightarrow (\lambda (H4: (eq A (AHead a3 a5) (AHead (AHead a a0)
560 a2))).(\lambda (H5: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).((let H6
561 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
562 with [(ASort _ _) \Rightarrow a5 | (AHead _ a7) \Rightarrow a7])) (AHead a3
563 a5) (AHead (AHead a a0) a2) H4) in ((let H7 \def (f_equal A A (\lambda (e:
564 A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a3 |
565 (AHead a7 _) \Rightarrow a7])) (AHead a3 a5) (AHead (AHead a a0) a2) H4) in
566 (eq_ind A (AHead a a0) (\lambda (a7: A).((eq A a5 a2) \to ((eq A (AHead a4
567 a6) (AHead a (asucc g a0))) \to ((leq g a7 a4) \to ((leq g a5 a6) \to P)))))
568 (\lambda (H8: (eq A a5 a2)).(eq_ind A a2 (\lambda (a7: A).((eq A (AHead a4
569 a6) (AHead a (asucc g a0))) \to ((leq g (AHead a a0) a4) \to ((leq g a7 a6)
570 \to P)))) (\lambda (H9: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).(let H10
571 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
572 with [(ASort _ _) \Rightarrow a6 | (AHead _ a7) \Rightarrow a7])) (AHead a4
573 a6) (AHead a (asucc g a0)) H9) in ((let H11 \def (f_equal A A (\lambda (e:
574 A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 |
575 (AHead a7 _) \Rightarrow a7])) (AHead a4 a6) (AHead a (asucc g a0)) H9) in
576 (eq_ind A a (\lambda (a7: A).((eq A a6 (asucc g a0)) \to ((leq g (AHead a a0)
577 a7) \to ((leq g a2 a6) \to P)))) (\lambda (H12: (eq A a6 (asucc g
578 a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((leq g (AHead a a0) a) \to
579 ((leq g a2 a7) \to P))) (\lambda (H13: (leq g (AHead a a0) a)).(\lambda (_:
580 (leq g a2 (asucc g a0))).(leq_ahead_false g a a0 H13 P))) a6 (sym_eq A a6
581 (asucc g a0) H12))) a4 (sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8)))
582 a3 (sym_eq A a3 (AHead a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A
583 (AHead (AHead a a0) a2)) (refl_equal A (AHead a (asucc g a0)))))))))))) a1)).
585 theorem leq_asucc_false:
586 \forall (g: G).(\forall (a: A).((leq g (asucc g a) a) \to (\forall (P:
589 \lambda (g: G).(\lambda (a: A).(A_ind (\lambda (a0: A).((leq g (asucc g a0)
590 a0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda
591 (H: (leq g (match n with [O \Rightarrow (ASort O (next g n0)) | (S h)
592 \Rightarrow (ASort h n0)]) (ASort n n0))).(\lambda (P: Prop).((match n in nat
593 return (\lambda (n1: nat).((leq g (match n1 with [O \Rightarrow (ASort O
594 (next g n0)) | (S h) \Rightarrow (ASort h n0)]) (ASort n1 n0)) \to P)) with
595 [O \Rightarrow (\lambda (H0: (leq g (ASort O (next g n0)) (ASort O n0))).(let
596 H1 \def (match H0 in leq return (\lambda (a0: A).(\lambda (a1: A).(\lambda
597 (_: (leq ? a0 a1)).((eq A a0 (ASort O (next g n0))) \to ((eq A a1 (ASort O
598 n0)) \to P))))) with [(leq_sort h1 h2 n1 n2 k H1) \Rightarrow (\lambda (H2:
599 (eq A (ASort h1 n1) (ASort O (next g n0)))).(\lambda (H3: (eq A (ASort h2 n2)
600 (ASort O n0))).((let H4 \def (f_equal A nat (\lambda (e: A).(match e in A
601 return (\lambda (_: A).nat) with [(ASort _ n3) \Rightarrow n3 | (AHead _ _)
602 \Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H2) in ((let H5 \def
603 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
604 [(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow h1])) (ASort h1 n1)
605 (ASort O (next g n0)) H2) in (eq_ind nat O (\lambda (n3: nat).((eq nat n1
606 (next g n0)) \to ((eq A (ASort h2 n2) (ASort O n0)) \to ((eq A (aplus g
607 (ASort n3 n1) k) (aplus g (ASort h2 n2) k)) \to P)))) (\lambda (H6: (eq nat
608 n1 (next g n0))).(eq_ind nat (next g n0) (\lambda (n3: nat).((eq A (ASort h2
609 n2) (ASort O n0)) \to ((eq A (aplus g (ASort O n3) k) (aplus g (ASort h2 n2)
610 k)) \to P))) (\lambda (H7: (eq A (ASort h2 n2) (ASort O n0))).(let H8 \def
611 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
612 [(ASort _ n3) \Rightarrow n3 | (AHead _ _) \Rightarrow n2])) (ASort h2 n2)
613 (ASort O n0) H7) in ((let H9 \def (f_equal A nat (\lambda (e: A).(match e in
614 A return (\lambda (_: A).nat) with [(ASort n3 _) \Rightarrow n3 | (AHead _ _)
615 \Rightarrow h2])) (ASort h2 n2) (ASort O n0) H7) in (eq_ind nat O (\lambda
616 (n3: nat).((eq nat n2 n0) \to ((eq A (aplus g (ASort O (next g n0)) k) (aplus
617 g (ASort n3 n2) k)) \to P))) (\lambda (H10: (eq nat n2 n0)).(eq_ind nat n0
618 (\lambda (n3: nat).((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort O
619 n3) k)) \to P)) (\lambda (H11: (eq A (aplus g (ASort O (next g n0)) k) (aplus
620 g (ASort O n0) k))).(let H12 \def (eq_ind_r A (aplus g (ASort O (next g n0))
621 k) (\lambda (a0: A).(eq A a0 (aplus g (ASort O n0) k))) H11 (aplus g (ASort O
622 n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let H_y \def (aplus_inj g (S k)
623 k (ASort O n0) H12) in (le_Sx_x k (eq_ind_r nat k (\lambda (n3: nat).(le n3
624 k)) (le_n k) (S k) H_y) P)))) n2 (sym_eq nat n2 n0 H10))) h2 (sym_eq nat h2 O
625 H9))) H8))) n1 (sym_eq nat n1 (next g n0) H6))) h1 (sym_eq nat h1 O H5)))
626 H4)) H3 H1))) | (leq_head a1 a2 H1 a3 a4 H2) \Rightarrow (\lambda (H3: (eq A
627 (AHead a1 a3) (ASort O (next g n0)))).(\lambda (H4: (eq A (AHead a2 a4)
628 (ASort O n0))).((let H5 \def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e
629 in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False |
630 (AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H3) in (False_ind
631 ((eq A (AHead a2 a4) (ASort O n0)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to
632 P))) H5)) H4 H1 H2)))]) in (H1 (refl_equal A (ASort O (next g n0)))
633 (refl_equal A (ASort O n0))))) | (S n1) \Rightarrow (\lambda (H0: (leq g
634 (ASort n1 n0) (ASort (S n1) n0))).(let H1 \def (match H0 in leq return
635 (\lambda (a0: A).(\lambda (a1: A).(\lambda (_: (leq ? a0 a1)).((eq A a0
636 (ASort n1 n0)) \to ((eq A a1 (ASort (S n1) n0)) \to P))))) with [(leq_sort h1
637 h2 n2 n3 k H1) \Rightarrow (\lambda (H2: (eq A (ASort h1 n2) (ASort n1
638 n0))).(\lambda (H3: (eq A (ASort h2 n3) (ASort (S n1) n0))).((let H4 \def
639 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
640 [(ASort _ n4) \Rightarrow n4 | (AHead _ _) \Rightarrow n2])) (ASort h1 n2)
641 (ASort n1 n0) H2) in ((let H5 \def (f_equal A nat (\lambda (e: A).(match e in
642 A return (\lambda (_: A).nat) with [(ASort n4 _) \Rightarrow n4 | (AHead _ _)
643 \Rightarrow h1])) (ASort h1 n2) (ASort n1 n0) H2) in (eq_ind nat n1 (\lambda
644 (n4: nat).((eq nat n2 n0) \to ((eq A (ASort h2 n3) (ASort (S n1) n0)) \to
645 ((eq A (aplus g (ASort n4 n2) k) (aplus g (ASort h2 n3) k)) \to P))))
646 (\lambda (H6: (eq nat n2 n0)).(eq_ind nat n0 (\lambda (n4: nat).((eq A (ASort
647 h2 n3) (ASort (S n1) n0)) \to ((eq A (aplus g (ASort n1 n4) k) (aplus g
648 (ASort h2 n3) k)) \to P))) (\lambda (H7: (eq A (ASort h2 n3) (ASort (S n1)
649 n0))).(let H8 \def (f_equal A nat (\lambda (e: A).(match e in A return
650 (\lambda (_: A).nat) with [(ASort _ n4) \Rightarrow n4 | (AHead _ _)
651 \Rightarrow n3])) (ASort h2 n3) (ASort (S n1) n0) H7) in ((let H9 \def
652 (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with
653 [(ASort n4 _) \Rightarrow n4 | (AHead _ _) \Rightarrow h2])) (ASort h2 n3)
654 (ASort (S n1) n0) H7) in (eq_ind nat (S n1) (\lambda (n4: nat).((eq nat n3
655 n0) \to ((eq A (aplus g (ASort n1 n0) k) (aplus g (ASort n4 n3) k)) \to P)))
656 (\lambda (H10: (eq nat n3 n0)).(eq_ind nat n0 (\lambda (n4: nat).((eq A
657 (aplus g (ASort n1 n0) k) (aplus g (ASort (S n1) n4) k)) \to P)) (\lambda
658 (H11: (eq A (aplus g (ASort n1 n0) k) (aplus g (ASort (S n1) n0) k))).(let
659 H12 \def (eq_ind_r A (aplus g (ASort n1 n0) k) (\lambda (a0: A).(eq A a0
660 (aplus g (ASort (S n1) n0) k))) H11 (aplus g (ASort (S n1) n0) (S k))
661 (aplus_sort_S_S_simpl g n0 n1 k)) in (let H_y \def (aplus_inj g (S k) k
662 (ASort (S n1) n0) H12) in (le_Sx_x k (eq_ind_r nat k (\lambda (n4: nat).(le
663 n4 k)) (le_n k) (S k) H_y) P)))) n3 (sym_eq nat n3 n0 H10))) h2 (sym_eq nat
664 h2 (S n1) H9))) H8))) n2 (sym_eq nat n2 n0 H6))) h1 (sym_eq nat h1 n1 H5)))
665 H4)) H3 H1))) | (leq_head a1 a2 H1 a3 a4 H2) \Rightarrow (\lambda (H3: (eq A
666 (AHead a1 a3) (ASort n1 n0))).(\lambda (H4: (eq A (AHead a2 a4) (ASort (S n1)
667 n0))).((let H5 \def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e in A
668 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
669 _) \Rightarrow True])) I (ASort n1 n0) H3) in (False_ind ((eq A (AHead a2 a4)
670 (ASort (S n1) n0)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to P))) H5)) H4 H1
671 H2)))]) in (H1 (refl_equal A (ASort n1 n0)) (refl_equal A (ASort (S n1)
672 n0)))))]) H))))) (\lambda (a0: A).(\lambda (_: (((leq g (asucc g a0) a0) \to
673 (\forall (P: Prop).P)))).(\lambda (a1: A).(\lambda (H0: (((leq g (asucc g a1)
674 a1) \to (\forall (P: Prop).P)))).(\lambda (H1: (leq g (AHead a0 (asucc g a1))
675 (AHead a0 a1))).(\lambda (P: Prop).(let H2 \def (match H1 in leq return
676 (\lambda (a2: A).(\lambda (a3: A).(\lambda (_: (leq ? a2 a3)).((eq A a2
677 (AHead a0 (asucc g a1))) \to ((eq A a3 (AHead a0 a1)) \to P))))) with
678 [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n1)
679 (AHead a0 (asucc g a1)))).(\lambda (H4: (eq A (ASort h2 n2) (AHead a0
680 a1))).((let H5 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A
681 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _)
682 \Rightarrow False])) I (AHead a0 (asucc g a1)) H3) in (False_ind ((eq A
683 (ASort h2 n2) (AHead a0 a1)) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g
684 (ASort h2 n2) k)) \to P)) H5)) H4 H2))) | (leq_head a2 a3 H2 a4 a5 H3)
685 \Rightarrow (\lambda (H4: (eq A (AHead a2 a4) (AHead a0 (asucc g
686 a1)))).(\lambda (H5: (eq A (AHead a3 a5) (AHead a0 a1))).((let H6 \def
687 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
688 [(ASort _ _) \Rightarrow a4 | (AHead _ a6) \Rightarrow a6])) (AHead a2 a4)
689 (AHead a0 (asucc g a1)) H4) in ((let H7 \def (f_equal A A (\lambda (e:
690 A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a2 |
691 (AHead a6 _) \Rightarrow a6])) (AHead a2 a4) (AHead a0 (asucc g a1)) H4) in
692 (eq_ind A a0 (\lambda (a6: A).((eq A a4 (asucc g a1)) \to ((eq A (AHead a3
693 a5) (AHead a0 a1)) \to ((leq g a6 a3) \to ((leq g a4 a5) \to P))))) (\lambda
694 (H8: (eq A a4 (asucc g a1))).(eq_ind A (asucc g a1) (\lambda (a6: A).((eq A
695 (AHead a3 a5) (AHead a0 a1)) \to ((leq g a0 a3) \to ((leq g a6 a5) \to P))))
696 (\lambda (H9: (eq A (AHead a3 a5) (AHead a0 a1))).(let H10 \def (f_equal A A
697 (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _)
698 \Rightarrow a5 | (AHead _ a6) \Rightarrow a6])) (AHead a3 a5) (AHead a0 a1)
699 H9) in ((let H11 \def (f_equal A A (\lambda (e: A).(match e in A return
700 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a3 | (AHead a6 _)
701 \Rightarrow a6])) (AHead a3 a5) (AHead a0 a1) H9) in (eq_ind A a0 (\lambda
702 (a6: A).((eq A a5 a1) \to ((leq g a0 a6) \to ((leq g (asucc g a1) a5) \to
703 P)))) (\lambda (H12: (eq A a5 a1)).(eq_ind A a1 (\lambda (a6: A).((leq g a0
704 a0) \to ((leq g (asucc g a1) a6) \to P))) (\lambda (_: (leq g a0
705 a0)).(\lambda (H14: (leq g (asucc g a1) a1)).(H0 H14 P))) a5 (sym_eq A a5 a1
706 H12))) a3 (sym_eq A a3 a0 H11))) H10))) a4 (sym_eq A a4 (asucc g a1) H8))) a2
707 (sym_eq A a2 a0 H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead a0
708 (asucc g a1))) (refl_equal A (AHead a0 a1)))))))))) a)).
projects / helm.git / blob