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