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/clen/defs.ma".
19 include "basic_1/getl/props.ma".
21 lemma getl_ctail_clen:
22 \forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n:
23 nat).(getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t))))))
25 \lambda (b: B).(\lambda (t: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(ex
26 nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort n)
27 (Bind b) t))))) (\lambda (n: nat).(ex_intro nat (\lambda (n0: nat).(getl O
28 (CHead (CSort n) (Bind b) t) (CHead (CSort n0) (Bind b) t))) n (getl_refl b
29 (CSort n) t))) (\lambda (c0: C).(\lambda (H: (ex nat (\lambda (n: nat).(getl
30 (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))))).(\lambda (k:
31 K).(\lambda (t0: T).(let H0 \def H in (ex_ind nat (\lambda (n: nat).(getl
32 (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))) (ex nat
33 (\lambda (n: nat).(getl (s k (clen c0)) (CHead (CTail (Bind b) t c0) k t0)
34 (CHead (CSort n) (Bind b) t)))) (\lambda (x: nat).(\lambda (H1: (getl (clen
35 c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t))).(K_ind (\lambda (k0:
36 K).(ex nat (\lambda (n: nat).(getl (s k0 (clen c0)) (CHead (CTail (Bind b) t
37 c0) k0 t0) (CHead (CSort n) (Bind b) t))))) (\lambda (b0: B).(ex_intro nat
38 (\lambda (n: nat).(getl (S (clen c0)) (CHead (CTail (Bind b) t c0) (Bind b0)
39 t0) (CHead (CSort n) (Bind b) t))) x (getl_head (Bind b0) (clen c0) (CTail
40 (Bind b) t c0) (CHead (CSort x) (Bind b) t) H1 t0))) (\lambda (f:
41 F).(ex_intro nat (\lambda (n: nat).(getl (clen c0) (CHead (CTail (Bind b) t
42 c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x (getl_flat (CTail (Bind b)
43 t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f t0))) k))) H0)))))) c))).
46 \forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall
47 (c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2
48 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
49 (\lambda (e: C).(getl i c1 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
50 nat).(eq nat i (clen c1))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
51 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))))))
53 \lambda (k: K).(\lambda (b: B).(\lambda (u1: T).(\lambda (u2: T).(\lambda
54 (c2: C).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (i: nat).((getl i
55 (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C
56 c2 (CTail k u1 e))) (\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4
57 nat (\lambda (_: nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind
58 b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort
59 n)))))))) (\lambda (n: nat).(\lambda (i: nat).(nat_ind (\lambda (n0:
60 nat).((getl n0 (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)) \to (or (ex2 C
61 (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n0 (CSort n)
62 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0 (clen (CSort
63 n)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2))
64 (\lambda (n1: nat).(eq C c2 (CSort n1))))))) (\lambda (H: (getl O (CHead
65 (CSort n) k u1) (CHead c2 (Bind b) u2))).(K_ind (\lambda (k0: K).((clear
66 (CHead (CSort n) k0 u1) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e:
67 C).(eq C c2 (CTail k0 u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e
68 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_:
69 nat).(eq K k0 (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0:
70 nat).(eq C c2 (CSort n0))))))) (\lambda (b0: B).(\lambda (H0: (clear (CHead
71 (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2))).(let H1 \def (f_equal C C
72 (\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 | (CHead c _ _)
73 \Rightarrow c])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
74 (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in ((let H2 \def
75 (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow b | (CHead
76 _ k0 _) \Rightarrow (match k0 with [(Bind b1) \Rightarrow b1 | (Flat _)
77 \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
78 (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in ((let H3 \def
79 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u2 | (CHead
80 _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
81 (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in (\lambda (H4:
82 (eq B b b0)).(\lambda (H5: (eq C c2 (CSort n))).(eq_ind_r C (CSort n)
83 (\lambda (c: C).(or (ex2 C (\lambda (e: C).(eq C c (CTail (Bind b0) u1 e)))
84 (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda
85 (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b))) (\lambda
86 (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c (CSort n0)))))) (eq_ind_r T
87 u1 (\lambda (t: T).(or (ex2 C (\lambda (e: C).(eq C (CSort n) (CTail (Bind
88 b0) u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) t)))) (ex4
89 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind
90 b))) (\lambda (_: nat).(eq T u1 t)) (\lambda (n0: nat).(eq C (CSort n) (CSort
91 n0)))))) (eq_ind_r B b0 (\lambda (b1: B).(or (ex2 C (\lambda (e: C).(eq C
92 (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e
93 (Bind b1) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_:
94 nat).(eq K (Bind b0) (Bind b1))) (\lambda (_: nat).(eq T u1 u1)) (\lambda
95 (n0: nat).(eq C (CSort n) (CSort n0)))))) (or_intror (ex2 C (\lambda (e:
96 C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n)
97 (CHead e (Bind b0) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda
98 (_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq T u1 u1)) (\lambda
99 (n0: nat).(eq C (CSort n) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq
100 nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq
101 T u1 u1)) (\lambda (n0: nat).(eq C (CSort n) (CSort n0))) n (refl_equal nat
102 O) (refl_equal K (Bind b0)) (refl_equal T u1) (refl_equal C (CSort n)))) b
103 H4) u2 H3) c2 H5)))) H2)) H1)))) (\lambda (f: F).(\lambda (H0: (clear (CHead
104 (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2))).(clear_gen_sort (CHead c2
105 (Bind b) u2) n (clear_gen_flat f (CSort n) (CHead c2 (Bind b) u2) u1 H0) (or
106 (ex2 C (\lambda (e: C).(eq C c2 (CTail (Flat f) u1 e))) (\lambda (e: C).(getl
107 O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O O))
108 (\lambda (_: nat).(eq K (Flat f) (Bind b))) (\lambda (_: nat).(eq T u1 u2))
109 (\lambda (n0: nat).(eq C c2 (CSort n0)))))))) k (getl_gen_O (CHead (CSort n)
110 k u1) (CHead c2 (Bind b) u2) H))) (\lambda (n0: nat).(\lambda (_: (((getl n0
111 (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e:
112 C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n0 (CSort n) (CHead e
113 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0 O)) (\lambda (_:
114 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n1:
115 nat).(eq C c2 (CSort n1)))))))).(\lambda (H0: (getl (S n0) (CHead (CSort n) k
116 u1) (CHead c2 (Bind b) u2))).(getl_gen_sort n (r k n0) (CHead c2 (Bind b) u2)
117 (getl_gen_S k (CSort n) (CHead c2 (Bind b) u2) u1 n0 H0) (or (ex2 C (\lambda
118 (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n0) (CSort n)
119 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n0) O))
120 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
121 (n1: nat).(eq C c2 (CSort n1))))))))) i))) (\lambda (c: C).(\lambda (H:
122 ((\forall (i: nat).((getl i (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or
123 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl i c
124 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat i (clen c)))
125 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
126 (n: nat).(eq C c2 (CSort n))))))))).(\lambda (k0: K).(\lambda (t: T).(\lambda
127 (i: nat).(nat_ind (\lambda (n: nat).((getl n (CTail k u1 (CHead c k0 t))
128 (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
129 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat
130 (\lambda (_: nat).(eq nat n (clen (CHead c k0 t)))) (\lambda (_: nat).(eq K k
131 (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort
132 n0))))))) (\lambda (H0: (getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind
133 b) u2))).(K_ind (\lambda (k1: K).((clear (CHead (CTail k u1 c) k1 t) (CHead
134 c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
135 (\lambda (e: C).(getl O (CHead c k1 t) (CHead e (Bind b) u2)))) (ex4 nat
136 (\lambda (_: nat).(eq nat O (s k1 (clen c)))) (\lambda (_: nat).(eq K k (Bind
137 b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort
138 n))))))) (\lambda (b0: B).(\lambda (H1: (clear (CHead (CTail k u1 c) (Bind
139 b0) t) (CHead c2 (Bind b) u2))).(let H2 \def (f_equal C C (\lambda (e:
140 C).(match e with [(CSort _) \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0]))
141 (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t) (clear_gen_bind b0
142 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) in ((let H3 \def (f_equal C B
143 (\lambda (e: C).(match e with [(CSort _) \Rightarrow b | (CHead _ k1 _)
144 \Rightarrow (match k1 with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow
145 b])])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
146 (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) in ((let H4
147 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u2 |
148 (CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c)
149 (Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1))
150 in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C c2 (CTail k u1 c))).(eq_ind
151 T u2 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
152 (\lambda (e: C).(getl O (CHead c (Bind b0) t0) (CHead e (Bind b) u2)))) (ex4
153 nat (\lambda (_: nat).(eq nat O (s (Bind b0) (clen c)))) (\lambda (_:
154 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
155 C c2 (CSort n)))))) (eq_ind B b (\lambda (b1: B).(or (ex2 C (\lambda (e:
156 C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b1) u2)
157 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b1)
158 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
159 u2)) (\lambda (n: nat).(eq C c2 (CSort n)))))) (let H7 \def (eq_ind C c2
160 (\lambda (c0: C).(\forall (i0: nat).((getl i0 (CTail k u1 c) (CHead c0 (Bind
161 b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e:
162 C).(getl i0 c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat i0
163 (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
164 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))))) H (CTail k u1 c) H6) in
165 (eq_ind_r C (CTail k u1 c) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C
166 c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) (CHead e
167 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b) (clen c))))
168 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
169 (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e: C).(eq C
170 (CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2)
171 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b)
172 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
173 u2)) (\lambda (n: nat).(eq C (CTail k u1 c) (CSort n)))) (ex_intro2 C
174 (\lambda (e: C).(eq C (CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O
175 (CHead c (Bind b) u2) (CHead e (Bind b) u2))) c (refl_equal C (CTail k u1 c))
176 (getl_refl b c u2))) c2 H6)) b0 H5) t H4)))) H3)) H2)))) (\lambda (f:
177 F).(\lambda (H1: (clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b)
178 u2))).(let H2 \def (H O (getl_intro O (CTail k u1 c) (CHead c2 (Bind b) u2)
179 (CTail k u1 c) (drop_refl (CTail k u1 c)) (clear_gen_flat f (CTail k u1 c)
180 (CHead c2 (Bind b) u2) t H1))) in (or_ind (ex2 C (\lambda (e: C).(eq C c2
181 (CTail k u1 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2)))) (ex4 nat
182 (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind b)))
183 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n)))) (or
184 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O
185 (CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
186 nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda
187 (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (H3:
188 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O c
189 (CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1
190 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2))) (or (ex2 C (\lambda
191 (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
192 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
193 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
194 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (x: C).(\lambda (H4:
195 (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x (Bind b)
196 u2))).(eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e:
197 C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
198 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
199 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
200 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e:
201 C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
202 (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
203 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
204 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C (CTail k u1 x) (CSort n))))
205 (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda
206 (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))) x (refl_equal C
207 (CTail k u1 x)) (getl_flat c (CHead x (Bind b) u2) O H5 f t))) c2 H4)))) H3))
208 (\lambda (H3: (ex4 nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_:
209 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
210 C c2 (CSort n))))).(ex4_ind nat (\lambda (_: nat).(eq nat O (clen c)))
211 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
212 (n: nat).(eq C c2 (CSort n))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
213 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))))
214 (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_:
215 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
216 C c2 (CSort n))))) (\lambda (x0: nat).(\lambda (H4: (eq nat O (clen
217 c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda
218 (H7: (eq C c2 (CSort x0))).(eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C
219 (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
220 (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
221 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
222 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (eq_ind T u1
223 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k u1 e)))
224 (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) t0)))) (ex4
225 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
226 K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n: nat).(eq C (CSort
227 x0) (CSort n)))))) (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda
228 (e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl O (CHead c
229 (Flat f) t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
230 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_:
231 nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))))))
232 (or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e)))
233 (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)))) (ex4
234 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
235 K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n: nat).(eq C
236 (CSort x0) (CSort n)))) (ex4_intro nat (\lambda (_: nat).(eq nat O (s (Flat
237 f) (clen c)))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_:
238 nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))) x0 H4
239 (refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) k H5)
240 u2 H6) c2 H7)))))) H3)) H2)))) k0 (getl_gen_O (CHead (CTail k u1 c) k0 t)
241 (CHead c2 (Bind b) u2) H0))) (\lambda (n: nat).(\lambda (H0: (((getl n (CHead
242 (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e:
243 C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e
244 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen c))))
245 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
246 (n0: nat).(eq C c2 (CSort n0)))))))).(\lambda (H1: (getl (S n) (CHead (CTail
247 k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let H_x \def (H (r k0 n) (getl_gen_S
248 k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H1)) in (let H2 \def H_x in
249 (or_ind (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e:
250 C).(getl (r k0 n) c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
251 nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
252 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))) (or (ex2 C
253 (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
254 c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
255 k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
256 u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (H3: (ex2 C
257 (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0 n) c
258 (CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1
259 e))) (\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))) (or (ex2 C
260 (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
261 c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
262 k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
263 u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x: C).(\lambda
264 (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl (r k0 n) c (CHead x (Bind
265 b) u2))).(let H6 \def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k
266 u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind
267 b) u2) t n H1) (CTail k u1 x) H4) in (let H7 \def (eq_ind C c2 (\lambda (c0:
268 C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 (Bind b) u2)) \to (or (ex2
269 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c
270 k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0
271 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
272 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0))))))) H0 (CTail k u1 x) H4) in
273 (eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C
274 c0 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind
275 b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda
276 (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0:
277 nat).(eq C c0 (CSort n0)))))) (or_introl (ex2 C (\lambda (e: C).(eq C (CTail
278 k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e
279 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c))))
280 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
281 (n0: nat).(eq C (CTail k u1 x) (CSort n0)))) (ex_intro2 C (\lambda (e: C).(eq
282 C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t)
283 (CHead e (Bind b) u2))) x (refl_equal C (CTail k u1 x)) (getl_head k0 n c
284 (CHead x (Bind b) u2) H5 t))) c2 H4)))))) H3)) (\lambda (H3: (ex4 nat
285 (\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind
286 b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort
287 n0))))).(ex4_ind nat (\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda
288 (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0:
289 nat).(eq C c2 (CSort n0))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
290 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4
291 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K
292 k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2
293 (CSort n0))))) (\lambda (x0: nat).(\lambda (H4: (eq nat (r k0 n) (clen
294 c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda
295 (H7: (eq C c2 (CSort x0))).(let H8 \def (eq_ind C c2 (\lambda (c0: C).(getl
296 (r k0 n) (CTail k u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1
297 c) (CHead c2 (Bind b) u2) t n H1) (CSort x0) H7) in (let H9 \def (eq_ind C c2
298 (\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 (Bind b) u2))
299 \to (or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e:
300 C).(getl n (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
301 nat).(eq nat n (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b)))
302 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0)))))))
303 H0 (CSort x0) H7) in (eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C
304 (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
305 c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
306 k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
307 u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0)))))) (let H10 \def (eq_ind_r T
308 u2 (\lambda (t0: T).((getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0)
309 (Bind b) t0)) \to (or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k u1
310 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind b) t0)))) (ex4 nat
311 (\lambda (_: nat).(eq nat n (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind
312 b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n0: nat).(eq C (CSort x0)
313 (CSort n0))))))) H9 u1 H6) in (let H11 \def (eq_ind_r T u2 (\lambda (t0:
314 T).(getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) t0))) H8 u1 H6)
315 in (eq_ind T u1 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C (CSort x0)
316 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b)
317 t0)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda
318 (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n0:
319 nat).(eq C (CSort x0) (CSort n0)))))) (let H12 \def (eq_ind K k (\lambda (k1:
320 K).((getl n (CHead (CTail k1 u1 c) k0 t) (CHead (CSort x0) (Bind b) u1)) \to
321 (or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e:
322 C).(getl n (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_:
323 nat).(eq nat n (s k0 (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b)))
324 (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort
325 n0))))))) H10 (Bind b) H5) in (let H13 \def (eq_ind K k (\lambda (k1:
326 K).(getl (r k0 n) (CTail k1 u1 c) (CHead (CSort x0) (Bind b) u1))) H11 (Bind
327 b) H5) in (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda (e:
328 C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0
329 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0
330 (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1
331 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0)))))) (eq_ind nat (r k0 n)
332 (\lambda (n0: nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind
333 b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b)
334 u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 n0))) (\lambda (_:
335 nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1:
336 nat).(eq C (CSort x0) (CSort n1)))))) (eq_ind_r nat (S n) (\lambda (n0:
337 nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e)))
338 (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat
339 (\lambda (_: nat).(eq nat (S n) n0)) (\lambda (_: nat).(eq K (Bind b) (Bind
340 b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1: nat).(eq C (CSort x0)
341 (CSort n1)))))) (or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail
342 (Bind b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b)
343 u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (S n))) (\lambda (_: nat).(eq
344 K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq
345 C (CSort x0) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat (S n) (S
346 n))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1
347 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0))) x0 (refl_equal nat (S
348 n)) (refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s
349 k0 (r k0 n)) (s_r k0 n)) (clen c) H4) k H5))) u2 H6))) c2 H7)))))))) H3))
350 H2)))))) i)))))) c1)))))).