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/lift/fwd".
19 include "lift/defs.ma".
22 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort
25 \lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort
29 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T
30 (lift h d (TLRef n)) (TLRef n)))))
32 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (lt n
33 d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true
34 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T
35 (TLRef n)) (blt n d) (sym_equal bool (blt n d) true (lt_blt d n H)))))).
38 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T
39 (lift h d (TLRef n)) (TLRef (plus n h))))))
41 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (le d
42 n)).(eq_ind bool false (\lambda (b: bool).(eq T (TLRef (match b with [true
43 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h))))
44 (refl_equal T (TLRef (plus n h))) (blt n d) (sym_equal bool (blt n d) false
48 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
49 (d: nat).(eq T (lift h d (THead k u t)) (THead k (lift h d u) (lift h (s k d)
52 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
53 (d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).
56 \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
57 (d: nat).(eq T (lift h d (THead (Bind b) u t)) (THead (Bind b) (lift h d u)
58 (lift h (S d) t)))))))
60 \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
61 (d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).
64 \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
65 (d: nat).(eq T (lift h d (THead (Flat f) u t)) (THead (Flat f) (lift h d u)
68 \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
69 (d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).
71 theorem lift_gen_sort:
72 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).(\forall (t: T).((eq T
73 (TSort n) (lift h d t)) \to (eq T t (TSort n))))))
75 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (t: T).(T_ind
76 (\lambda (t0: T).((eq T (TSort n) (lift h d t0)) \to (eq T t0 (TSort n))))
77 (\lambda (n0: nat).(\lambda (H: (eq T (TSort n) (lift h d (TSort
78 n0)))).(sym_eq T (TSort n) (TSort n0) H))) (\lambda (n0: nat).(\lambda (H:
79 (eq T (TSort n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TSort
80 n)) (\lambda (H0: (lt n0 d)).(let H1 \def (eq_ind T (lift h d (TLRef n0))
81 (\lambda (t: T).(eq T (TSort n) t)) H (TLRef n0) (lift_lref_lt n0 h d H0)) in
82 (let H2 \def (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
83 t)).((eq T t (TLRef n0)) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal
84 \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef n0))).(let H2 \def (eq_ind T
85 (TSort n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
86 [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
87 \Rightarrow False])) I (TLRef n0) H1) in (False_ind (eq T (TLRef n0) (TSort
88 n)) H2)))]) in (H2 (refl_equal T (TLRef n0)))))) (\lambda (H0: (le d
89 n0)).(let H1 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T
90 (TSort n) t)) H (TLRef (plus n0 h)) (lift_lref_ge n0 h d H0)) in (let H2 \def
91 (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
92 (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal
93 \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef (plus n0 h)))).(let H2 \def
94 (eq_ind T (TSort n) (\lambda (e: T).(match e in T return (\lambda (_:
95 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
96 (THead _ _ _) \Rightarrow False])) I (TLRef (plus n0 h)) H1) in (False_ind
97 (eq T (TLRef n0) (TSort n)) H2)))]) in (H2 (refl_equal T (TLRef (plus n0
98 h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TSort n)
99 (lift h d t0)) \to (eq T t0 (TSort n))))).(\lambda (t1: T).(\lambda (_: (((eq
100 T (TSort n) (lift h d t1)) \to (eq T t1 (TSort n))))).(\lambda (H1: (eq T
101 (TSort n) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d
102 (THead k t0 t1)) (\lambda (t: T).(eq T (TSort n) t)) H1 (THead k (lift h d
103 t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2
104 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift
105 h d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TSort n))))) with
106 [refl_equal \Rightarrow (\lambda (H2: (eq T (TSort n) (THead k (lift h d t0)
107 (lift h (s k d) t1)))).(let H3 \def (eq_ind T (TSort n) (\lambda (e:
108 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
109 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
110 (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (eq T (THead k
111 t0 t1) (TSort n)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h
112 (s k d) t1)))))))))))) t)))).
114 theorem lift_gen_lref:
115 \forall (t: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T
116 (TLRef i) (lift h d t)) \to (or (land (lt i d) (eq T t (TLRef i))) (land (le
117 (plus d h) i) (eq T t (TLRef (minus i h)))))))))
119 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(\forall (h:
120 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d)
121 (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i
122 h)))))))))) (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda
123 (i: nat).(\lambda (H: (eq T (TLRef i) (lift h d (TSort n)))).(let H0 \def
124 (eq_ind T (lift h d (TSort n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TSort
125 n) (lift_sort n h d)) in (let H1 \def (eq_ind T (TLRef i) (\lambda (ee:
126 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
127 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
128 (TSort n) H0) in (False_ind (or (land (lt i d) (eq T (TSort n) (TLRef i)))
129 (land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h))))) H1))))))))
130 (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i:
131 nat).(\lambda (H: (eq T (TLRef i) (lift h d (TLRef n)))).(lt_le_e n d (or
132 (land (lt i d) (eq T (TLRef n) (TLRef i))) (land (le (plus d h) i) (eq T
133 (TLRef n) (TLRef (minus i h))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind
134 T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TLRef n)
135 (lift_lref_lt n h d H0)) in (let H2 \def (f_equal T nat (\lambda (e:
136 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i |
137 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n)
138 H1) in (eq_ind_r nat n (\lambda (n0: nat).(or (land (lt n0 d) (eq T (TLRef n)
139 (TLRef n0))) (land (le (plus d h) n0) (eq T (TLRef n) (TLRef (minus n0
140 h)))))) (or_introl (land (lt n d) (eq T (TLRef n) (TLRef n))) (land (le (plus
141 d h) n) (eq T (TLRef n) (TLRef (minus n h)))) (conj (lt n d) (eq T (TLRef n)
142 (TLRef n)) H0 (refl_equal T (TLRef n)))) i H2)))) (\lambda (H0: (le d
143 n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef
144 i) t)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (f_equal
145 T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort
146 _) \Rightarrow i | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i]))
147 (TLRef i) (TLRef (plus n h)) H1) in (eq_ind_r nat (plus n h) (\lambda (n0:
148 nat).(or (land (lt n0 d) (eq T (TLRef n) (TLRef n0))) (land (le (plus d h)
149 n0) (eq T (TLRef n) (TLRef (minus n0 h)))))) (eq_ind_r nat n (\lambda (n0:
150 nat).(or (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land
151 (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n0))))) (or_intror (land
152 (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land (le (plus d h)
153 (plus n h)) (eq T (TLRef n) (TLRef n))) (conj (le (plus d h) (plus n h)) (eq
154 T (TLRef n) (TLRef n)) (plus_le_compat d n h h H0 (le_n h)) (refl_equal T
155 (TLRef n)))) (minus (plus n h) h) (minus_plus_r n h)) i H2)))))))))) (\lambda
156 (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (d: nat).(\forall (h:
157 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d)
158 (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i
159 h))))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (d: nat).(\forall (h:
160 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t1)) \to (or (land (lt i d)
161 (eq T t1 (TLRef i))) (land (le (plus d h) i) (eq T t1 (TLRef (minus i
162 h))))))))))).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i: nat).(\lambda
163 (H1: (eq T (TLRef i) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T
164 (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef i) t)) H1 (THead k
165 (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def
166 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
167 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
168 (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d)
169 t1)) H2) in (False_ind (or (land (lt i d) (eq T (THead k t0 t1) (TLRef i)))
170 (land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))))
173 theorem lift_gen_lref_lt:
174 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((lt n d) \to (\forall
175 (t: T).((eq T (TLRef n) (lift h d t)) \to (eq T t (TLRef n)))))))
177 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (lt n
178 d)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef n) (lift h d t0))
179 \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef n)
180 (lift h d (TSort n0)))).(sym_eq T (TLRef n) (TSort n0) H0))) (\lambda (n0:
181 nat).(\lambda (H0: (eq T (TLRef n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq
182 T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0 d)).(let H2 \def (eq_ind T (lift
183 h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H0 (TLRef n0)
184 (lift_lref_lt n0 h d H1)) in (sym_eq T (TLRef n) (TLRef n0) H2))) (\lambda
185 (H1: (le d n0)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t:
186 T).(eq T (TLRef n) t)) H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in
187 (let H3 \def (match H2 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
188 t)).((eq T t (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TLRef n))))) with
189 [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef n) (TLRef (plus n0
190 h)))).(let H3 \def (f_equal T nat (\lambda (e: T).(match e in T return
191 (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n
192 | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef (plus n0 h)) H2) in (eq_ind
193 nat (plus n0 h) (\lambda (n: nat).(eq T (TLRef n0) (TLRef n))) (let H0 \def
194 (eq_ind nat n (\lambda (n: nat).(lt n d)) H (plus n0 h) H3) in (le_false d n0
195 (eq T (TLRef n0) (TLRef (plus n0 h))) H1 (lt_le_S n0 d (le_lt_trans n0 (plus
196 n0 h) d (le_plus_l n0 h) H0)))) n (sym_eq nat n (plus n0 h) H3))))]) in (H3
197 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0:
198 T).(\lambda (_: (((eq T (TLRef n) (lift h d t0)) \to (eq T t0 (TLRef
199 n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef n) (lift h d t1)) \to (eq
200 T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef n) (lift h d (THead k t0
201 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq
202 T (TLRef n) t)) H2 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k
203 t0 t1 h d)) in (let H4 \def (match H3 in eq return (\lambda (t: T).(\lambda
204 (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to (eq
205 T (THead k t0 t1) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H3:
206 (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H4 \def
207 (eq_ind T (TLRef n) (\lambda (e: T).(match e in T return (\lambda (_:
208 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
209 (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d)
210 t1)) H3) in (False_ind (eq T (THead k t0 t1) (TLRef n)) H4)))]) in (H4
211 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))) t))))).
213 theorem lift_gen_lref_false:
214 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n
215 (plus d h)) \to (\forall (t: T).((eq T (TLRef n) (lift h d t)) \to (\forall
218 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d
219 n)).(\lambda (H0: (lt n (plus d h))).(\lambda (t: T).(T_ind (\lambda (t0:
220 T).((eq T (TLRef n) (lift h d t0)) \to (\forall (P: Prop).P))) (\lambda (n0:
221 nat).(\lambda (H1: (eq T (TLRef n) (lift h d (TSort n0)))).(\lambda (P:
222 Prop).(let H2 \def (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ?
223 ? t)).((eq T t (lift h d (TSort n0))) \to P))) with [refl_equal \Rightarrow
224 (\lambda (H2: (eq T (TLRef n) (lift h d (TSort n0)))).(let H3 \def (eq_ind T
225 (TLRef n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
226 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
227 \Rightarrow False])) I (lift h d (TSort n0)) H2) in (False_ind P H3)))]) in
228 (H2 (refl_equal T (lift h d (TSort n0)))))))) (\lambda (n0: nat).(\lambda
229 (H1: (eq T (TLRef n) (lift h d (TLRef n0)))).(\lambda (P: Prop).(lt_le_e n0 d
230 P (\lambda (H2: (lt n0 d)).(let H3 \def (eq_ind T (lift h d (TLRef n0))
231 (\lambda (t: T).(eq T (TLRef n) t)) H1 (TLRef n0) (lift_lref_lt n0 h d H2))
232 in (let H4 \def (match H3 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
233 t)).((eq T t (TLRef n0)) \to P))) with [refl_equal \Rightarrow (\lambda (H3:
234 (eq T (TLRef n) (TLRef n0))).(let H4 \def (f_equal T nat (\lambda (e:
235 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
236 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef n0)
237 H3) in (eq_ind nat n0 (\lambda (_: nat).P) (let H1 \def (eq_ind_r nat n0
238 (\lambda (n: nat).(lt n d)) H2 n H4) in (le_false d n P H H1)) n (sym_eq nat
239 n n0 H4))))]) in (H4 (refl_equal T (TLRef n0)))))) (\lambda (H2: (le d
240 n0)).(let H3 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T
241 (TLRef n) t)) H1 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H2)) in (let H4
242 \def (match H3 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
243 (TLRef (plus n0 h))) \to P))) with [refl_equal \Rightarrow (\lambda (H3: (eq
244 T (TLRef n) (TLRef (plus n0 h)))).(let H4 \def (f_equal T nat (\lambda (e:
245 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
246 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef
247 (plus n0 h)) H3) in (eq_ind nat (plus n0 h) (\lambda (_: nat).P) (let H1 \def
248 (eq_ind nat n (\lambda (n: nat).(lt n (plus d h))) H0 (plus n0 h) H4) in
249 (le_false d n0 P H2 (lt_le_S n0 d (simpl_lt_plus_r h n0 d H1)))) n (sym_eq
250 nat n (plus n0 h) H4))))]) in (H4 (refl_equal T (TLRef (plus n0 h)))))))))))
251 (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef n) (lift h d
252 t0)) \to (\forall (P: Prop).P)))).(\lambda (t1: T).(\lambda (_: (((eq T
253 (TLRef n) (lift h d t1)) \to (\forall (P: Prop).P)))).(\lambda (H3: (eq T
254 (TLRef n) (lift h d (THead k t0 t1)))).(\lambda (P: Prop).(let H4 \def
255 (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef n) t)) H3
256 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let
257 H5 \def (match H4 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq
258 T t (THead k (lift h d t0) (lift h (s k d) t1))) \to P))) with [refl_equal
259 \Rightarrow (\lambda (H4: (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k
260 d) t1)))).(let H5 \def (eq_ind T (TLRef n) (\lambda (e: T).(match e in T
261 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
262 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d
263 t0) (lift h (s k d) t1)) H4) in (False_ind P H5)))]) in (H5 (refl_equal T
264 (THead k (lift h d t0) (lift h (s k d) t1))))))))))))) t)))))).
266 theorem lift_gen_lref_ge:
267 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall
268 (t: T).((eq T (TLRef (plus n h)) (lift h d t)) \to (eq T t (TLRef n)))))))
270 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d
271 n)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef (plus n h)) (lift h
272 d t0)) \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T
273 (TLRef (plus n h)) (lift h d (TSort n0)))).(let H1 \def (match H0 in eq
274 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (lift h d (TSort
275 n0))) \to (eq T (TSort n0) (TLRef n))))) with [refl_equal \Rightarrow
276 (\lambda (H1: (eq T (TLRef (plus n h)) (lift h d (TSort n0)))).(let H2 \def
277 (eq_ind T (TLRef (plus n h)) (\lambda (e: T).(match e in T return (\lambda
278 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
279 (THead _ _ _) \Rightarrow False])) I (lift h d (TSort n0)) H1) in (False_ind
280 (eq T (TSort n0) (TLRef n)) H2)))]) in (H1 (refl_equal T (lift h d (TSort
281 n0))))))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d
282 (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0
283 d)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef
284 (plus n h)) t)) H0 (TLRef n0) (lift_lref_lt n0 h d H1)) in (let H3 \def
285 (match H2 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
286 (TLRef n0)) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow
287 (\lambda (H2: (eq T (TLRef (plus n h)) (TLRef n0))).(let H3 \def (f_equal T
288 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
289 \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m:
290 nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in
291 plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec
292 plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O
293 \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef
294 (plus n h)) (TLRef n0) H2) in (eq_ind nat (plus n h) (\lambda (n0: nat).(eq T
295 (TLRef n0) (TLRef n))) (let H0 \def (eq_ind_r nat n0 (\lambda (n: nat).(lt n
296 d)) H1 (plus n h) H3) in (le_false d n (eq T (TLRef (plus n h)) (TLRef n)) H
297 (lt_le_S n d (le_lt_trans n (plus n h) d (le_plus_l n h) H0)))) n0 H3)))]) in
298 (H3 (refl_equal T (TLRef n0)))))) (\lambda (H1: (le d n0)).(let H2 \def
299 (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef (plus n h)) t))
300 H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in (let H3 \def (match H2 in
301 eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0
302 h))) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda
303 (H2: (eq T (TLRef (plus n h)) (TLRef (plus n0 h)))).(let H3 \def (f_equal T
304 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
305 \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m:
306 nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in
307 plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec
308 plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O
309 \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef
310 (plus n h)) (TLRef (plus n0 h)) H2) in (eq_ind nat (plus n h) (\lambda (_:
311 nat).(eq T (TLRef n0) (TLRef n))) (f_equal nat T TLRef n0 n (simpl_plus_r h
312 n0 n (sym_eq nat (plus n h) (plus n0 h) H3))) (plus n0 h) H3)))]) in (H3
313 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0:
314 T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t0)) \to (eq T t0 (TLRef
315 n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d
316 t1)) \to (eq T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef (plus n h)) (lift
317 h d (THead k t0 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1))
318 (\lambda (t: T).(eq T (TLRef (plus n h)) t)) H2 (THead k (lift h d t0) (lift
319 h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H4 \def (match H3 in eq
320 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d
321 t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with
322 [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef (plus n h)) (THead k (lift
323 h d t0) (lift h (s k d) t1)))).(let H4 \def (eq_ind T (TLRef (plus n h))
324 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
325 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
326 False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H3) in (False_ind (eq
327 T (THead k t0 t1) (TLRef n)) H4)))]) in (H4 (refl_equal T (THead k (lift h d
328 t0) (lift h (s k d) t1)))))))))))) t))))).
330 theorem lift_gen_head:
331 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
332 nat).(\forall (d: nat).((eq T (THead k u t) (lift h d x)) \to (ex3_2 T T
333 (\lambda (y: T).(\lambda (z: T).(eq T x (THead k y z)))) (\lambda (y:
334 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
335 T).(eq T t (lift h (s k d) z)))))))))))
337 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
338 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k u t)
339 (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead
340 k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
341 (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))))))) (\lambda (n:
342 nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k u t)
343 (lift h d (TSort n)))).(let H0 \def (match H in eq return (\lambda (t0:
344 T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2 T T
345 (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y:
346 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
347 T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda
348 (H0: (eq T (THead k u t) (lift h d (TSort n)))).(let H1 \def (eq_ind T (THead
349 k u t) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
350 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
351 \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T
352 (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y:
353 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
354 T).(eq T t (lift h (s k d) z))))) H1)))]) in (H0 (refl_equal T (lift h d
355 (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d:
356 nat).(\lambda (H: (eq T (THead k u t) (lift h d (TLRef n)))).(lt_le_e n d
357 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z))))
358 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
359 T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) (\lambda (H0: (lt n
360 d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead
361 k u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in
362 eq return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to
363 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z))))
364 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
365 T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal
366 \Rightarrow (\lambda (H1: (eq T (THead k u t) (TLRef n))).(let H2 \def
367 (eq_ind T (THead k u t) (\lambda (e: T).(match e in T return (\lambda (_:
368 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
369 (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
370 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y:
371 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
372 T).(eq T t (lift h (s k d) z))))) H2)))]) in (H2 (refl_equal T (TLRef n))))))
373 (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda
374 (t0: T).(eq T (THead k u t) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d
375 H0)) in (let H2 \def (match H1 in eq return (\lambda (t0: T).(\lambda (_: (eq
376 ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T T (\lambda (y:
377 T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda
378 (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift
379 h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead k
380 u t) (TLRef (plus n h)))).(let H2 \def (eq_ind T (THead k u t) (\lambda (e:
381 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
382 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
383 (TLRef (plus n h)) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z:
384 T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u
385 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d)
386 z))))) H2)))]) in (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda
387 (k0: K).(\lambda (t0: T).(\lambda (_: ((\forall (h: nat).(\forall (d:
388 nat).((eq T (THead k u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y:
389 T).(\lambda (z: T).(eq T t0 (THead k y z)))) (\lambda (y: T).(\lambda (_:
390 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s
391 k d) z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall
392 (d: nat).((eq T (THead k u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y:
393 T).(\lambda (z: T).(eq T t1 (THead k y z)))) (\lambda (y: T).(\lambda (_:
394 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s
395 k d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T
396 (THead k u t) (lift h d (THead k0 t0 t1)))).(let H2 \def (eq_ind T (lift h d
397 (THead k0 t0 t1)) (\lambda (t0: T).(eq T (THead k u t) t0)) H1 (THead k0
398 (lift h d t0) (lift h (s k0 d) t1)) (lift_head k0 t0 t1 h d)) in (let H3 \def
399 (match H2 in eq return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2
400 (THead k0 (lift h d t0) (lift h (s k0 d) t1))) \to (ex3_2 T T (\lambda (y:
401 T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y:
402 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
403 T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda
404 (H2: (eq T (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)))).(let
405 H3 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
406 with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t)
407 \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
408 H2) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
409 (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u |
410 (THead _ t _) \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h
411 (s k0 d) t1)) H2) in ((let H5 \def (f_equal T K (\lambda (e: T).(match e in T
412 return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
413 \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k u t) (THead k0 (lift
414 h d t0) (lift h (s k0 d) t1)) H2) in (eq_ind K k0 (\lambda (k: K).((eq T u
415 (lift h d t0)) \to ((eq T t (lift h (s k0 d) t1)) \to (ex3_2 T T (\lambda (y:
416 T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y:
417 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
418 T).(eq T t (lift h (s k d) z)))))))) (\lambda (H6: (eq T u (lift h d
419 t0))).(eq_ind T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s k0 d) t1))
420 \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead
421 k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda
422 (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z))))))) (\lambda (H7: (eq T
423 t (lift h (s k0 d) t1))).(eq_ind T (lift h (s k0 d) t1) (\lambda (t:
424 T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead
425 k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d
426 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z))))))
427 (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1)
428 (THead k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h
429 d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s k0 d) t1) (lift h (s
430 k0 d) z)))) t0 t1 (refl_equal T (THead k0 t0 t1)) (refl_equal T (lift h d
431 t0)) (refl_equal T (lift h (s k0 d) t1))) t (sym_eq T t (lift h (s k0 d) t1)
432 H7))) u (sym_eq T u (lift h d t0) H6))) k (sym_eq K k k0 H5))) H4)) H3)))])
433 in (H3 (refl_equal T (THead k0 (lift h d t0) (lift h (s k0 d)
434 t1)))))))))))))) x)))).
436 theorem lift_gen_bind:
437 \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
438 nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d x)) \to (ex3_2 T
439 T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda
440 (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
441 T).(eq T t (lift h (S d) z)))))))))))
443 \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
444 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u
445 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
446 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
447 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))))
448 (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T
449 (THead (Bind b) u t) (lift h d (TSort n)))).(let H0 \def (match H in eq
450 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort
451 n))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead
452 (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y))))
453 (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with
454 [refl_equal \Rightarrow (\lambda (H0: (eq T (THead (Bind b) u t) (lift h d
455 (TSort n)))).(let H1 \def (eq_ind T (THead (Bind b) u t) (\lambda (e:
456 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
457 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
458 (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda
459 (z: T).(eq T (TSort n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_:
460 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S
461 d) z))))) H1)))]) in (H0 (refl_equal T (lift h d (TSort n))))))))) (\lambda
462 (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind
463 b) u t) (lift h d (TLRef n)))).(lt_le_e n d (ex3_2 T T (\lambda (y:
464 T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y:
465 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
466 T).(eq T t (lift h (S d) z))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind
467 T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H
468 (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in eq return
469 (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to (ex3_2 T
470 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
471 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
472 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
473 \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef n))).(let H2 \def
474 (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e in T return (\lambda
475 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
476 | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
477 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
478 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
479 T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in (H2 (refl_equal T
480 (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d
481 (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H (TLRef (plus n
482 h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 in eq return (\lambda
483 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T
484 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
485 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
486 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
487 \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef (plus n
488 h)))).(let H2 \def (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e in
489 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
490 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h))
491 H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n)
492 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
493 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in
494 (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0:
495 T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u
496 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
497 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
498 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d)
499 z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall (d:
500 nat).((eq T (THead (Bind b) u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y:
501 T).(\lambda (z: T).(eq T t1 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda
502 (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift
503 h (S d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T
504 (THead (Bind b) u t) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T
505 (lift h d (THead k t0 t1)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0))
506 H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in
507 (let H3 \def (match H2 in eq return (\lambda (t2: T).(\lambda (_: (eq ? ?
508 t2)).((eq T t2 (THead k (lift h d t0) (lift h (s k d) t1))) \to (ex3_2 T T
509 (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Bind b) y z))))
510 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
511 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
512 \Rightarrow (\lambda (H2: (eq T (THead (Bind b) u t) (THead k (lift h d t0)
513 (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e: T).(match e in
514 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _)
515 \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Bind b) u t) (THead k
516 (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T (\lambda
517 (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u
518 | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Bind b) u
519 t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H5 \def (f_equal
520 T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
521 \Rightarrow (Bind b) | (TLRef _) \Rightarrow (Bind b) | (THead k _ _)
522 \Rightarrow k])) (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d)
523 t1)) H2) in (eq_ind K (Bind b) (\lambda (k: K).((eq T u (lift h d t0)) \to
524 ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z:
525 T).(eq T (THead k t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_:
526 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S
527 d) z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind T (lift h d t0)
528 (\lambda (t2: T).((eq T t (lift h (s (Bind b) d) t1)) \to (ex3_2 T T (\lambda
529 (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b) y z))))
530 (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda (_:
531 T).(\lambda (z: T).(eq T t (lift h (S d) z))))))) (\lambda (H7: (eq T t (lift
532 h (s (Bind b) d) t1))).(eq_ind T (lift h (s (Bind b) d) t1) (\lambda (t:
533 T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1)
534 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0)
535 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))))
536 (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1)
537 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0)
538 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Bind b) d)
539 t1) (lift h (S d) z)))) t0 t1 (refl_equal T (THead (Bind b) t0 t1))
540 (refl_equal T (lift h d t0)) (refl_equal T (lift h (S d) t1))) t (sym_eq T t
541 (lift h (s (Bind b) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5))
542 H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d)
543 t1)))))))))))))) x)))).
545 theorem lift_gen_flat:
546 \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
547 nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d x)) \to (ex3_2 T
548 T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda
549 (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
550 T).(eq T t (lift h d z)))))))))))
552 \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
553 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u
554 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
555 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
556 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))) (\lambda
557 (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Flat
558 f) u t) (lift h d (TSort n)))).(let H0 \def (match H in eq return (\lambda
559 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2
560 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y z))))
561 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
562 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
563 (\lambda (H0: (eq T (THead (Flat f) u t) (lift h d (TSort n)))).(let H1 \def
564 (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda
565 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
566 | (THead _ _ _) \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind
567 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y
568 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
569 T).(\lambda (z: T).(eq T t (lift h d z))))) H1)))]) in (H0 (refl_equal T
570 (lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d:
571 nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d (TLRef n)))).(lt_le_e
572 n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat
573 f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
574 (_: T).(\lambda (z: T).(eq T t (lift h d z))))) (\lambda (H0: (lt n d)).(let
575 H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f)
576 u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in
577 eq return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to
578 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
579 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
580 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
581 (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef n))).(let H2 \def (eq_ind T
582 (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda (_:
583 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
584 (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
585 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
586 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
587 T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T
588 (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d
589 (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H (TLRef (plus n
590 h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 in eq return (\lambda
591 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T
592 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
593 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
594 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
595 (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef (plus n h)))).(let H2 \def
596 (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda
597 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
598 | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H1) in (False_ind
599 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
600 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
601 T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T
602 (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_:
603 ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d
604 t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f)
605 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
606 T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (t1: T).(\lambda
607 (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h
608 d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Flat
609 f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
610 (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (h:
611 nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead (Flat f) u t) (lift h d
612 (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda
613 (t0: T).(eq T (THead (Flat f) u t) t0)) H1 (THead k (lift h d t0) (lift h (s
614 k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 in eq return
615 (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0)
616 (lift h (s k d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T
617 (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
618 u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))
619 with [refl_equal \Rightarrow (\lambda (H2: (eq T (THead (Flat f) u t) (THead
620 k (lift h d t0) (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e:
621 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t |
622 (TLRef _) \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Flat f) u t)
623 (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T
624 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
625 \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t]))
626 (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let
627 H5 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
628 with [(TSort _) \Rightarrow (Flat f) | (TLRef _) \Rightarrow (Flat f) |
629 (THead k _ _) \Rightarrow k])) (THead (Flat f) u t) (THead k (lift h d t0)
630 (lift h (s k d) t1)) H2) in (eq_ind K (Flat f) (\lambda (k: K).((eq T u (lift
631 h d t0)) \to ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y:
632 T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y:
633 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
634 T).(eq T t (lift h d z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind
635 T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s (Flat f) d) t1)) \to
636 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) t0 t1)
637 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d
638 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))) (\lambda
639 (H7: (eq T t (lift h (s (Flat f) d) t1))).(eq_ind T (lift h (s (Flat f) d)
640 t1) (\lambda (t: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead
641 (Flat f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
642 (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h
643 d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat
644 f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift
645 h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s
646 (Flat f) d) t1) (lift h d z)))) t0 t1 (refl_equal T (THead (Flat f) t0 t1))
647 (refl_equal T (lift h d t0)) (refl_equal T (lift h d t1))) t (sym_eq T t
648 (lift h (s (Flat f) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5))
649 H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d)
650 t1)))))))))))))) x)))).