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 "LambdaDelta-1/ty3/fwd.ma".
19 include "LambdaDelta-1/pc3/fwd.ma".
22 \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e
23 t1 t2) \to (\forall (c: C).(\forall (d: nat).(\forall (h: nat).((drop h d c
24 e) \to (ty3 g c (lift h d t1) (lift h d t2))))))))))
26 \lambda (g: G).(\lambda (e: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
27 (H: (ty3 g e t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda (t0:
28 T).(\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
29 (ty3 g c0 (lift h d t) (lift h d t0))))))))) (\lambda (c: C).(\lambda (t0:
30 T).(\lambda (t: T).(\lambda (_: (ty3 g c t0 t)).(\lambda (H1: ((\forall (c0:
31 C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h
32 d t0) (lift h d t)))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (_: (ty3
33 g c u t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
34 nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
35 t3)))))))).(\lambda (H4: (pc3 c t3 t0)).(\lambda (c0: C).(\lambda (d:
36 nat).(\lambda (h: nat).(\lambda (H5: (drop h d c0 c)).(ty3_conv g c0 (lift h
37 d t0) (lift h d t) (H1 c0 d h H5) (lift h d u) (lift h d t3) (H3 c0 d h H5)
38 (pc3_lift c0 c h d H5 t3 t0 H4)))))))))))))))) (\lambda (c: C).(\lambda (m:
39 nat).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (_: (drop
40 h d c0 c)).(eq_ind_r T (TSort m) (\lambda (t: T).(ty3 g c0 t (lift h d (TSort
41 (next g m))))) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(ty3 g c0
42 (TSort m) t)) (ty3_sort g c0 m) (lift h d (TSort (next g m))) (lift_sort
43 (next g m) h d)) (lift h d (TSort m)) (lift_sort m h d)))))))) (\lambda (n:
44 nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
45 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
46 t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
47 nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
48 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
49 (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
50 (lift (S n) O t))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
51 n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3 (CHead d (Bind Abbr) u) H0)
52 in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0)))
53 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n) e0 e1))) (\lambda (_:
54 C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0
55 (TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x0: C).(\lambda (x1:
56 C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
57 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind
58 nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S
59 n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0
60 (S n)) H9 Abbr d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1
61 (Bind Abbr) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h (minus d0
62 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
63 (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h (minus
64 d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x d)).(eq_ind_r T
65 (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t))))
66 (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3 g c0 (TLRef
67 n) (lift h n0 (lift (S n) O t)))) (eq_ind_r T (lift (S n) O (lift h (minus d0
68 (S n)) t)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda
69 (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))))
70 (ty3_abbr g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0 (CHead x
71 (Bind Abbr) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus d0 (S n))
72 t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
73 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
74 n) O t)) (lift_d t h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
75 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
76 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
77 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat
78 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
79 t)))) (eq_ind_r T (lift (plus h (S n)) O t) (\lambda (t0: T).(ty3 g c0 (TLRef
80 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
81 (TLRef (plus n h)) (lift n0 O t))) (ty3_abbr g (plus n h) c0 d u
82 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) t H1) (plus
83 h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
84 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
85 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
86 (plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
87 d0 H4)))))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d:
88 C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda
89 (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall
90 (d0: nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u)
91 (lift h d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h:
92 nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0
93 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5
94 \def (drop_getl_trans_le n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3
95 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_:
96 C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n)
97 e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst)
98 u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda
99 (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop
100 h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let
101 H9 \def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S
102 (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0
103 h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0
104 (CHead c1 (Bind Abst) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h
105 (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S
106 n) O u))) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift
107 h (minus d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x
108 d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S
109 n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3
110 g c0 (TLRef n) (lift h n0 (lift (S n) O u)))) (eq_ind_r T (lift (S n) O (lift
111 h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat
112 d0 (\lambda (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S
113 n)) u)))) (ty3_abst g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0
114 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus
115 d0 (S n)) t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
116 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
117 n) O u)) (lift_d u h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
118 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
119 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
120 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat
121 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
122 u)))) (eq_ind_r T (lift (plus h (S n)) O u) (\lambda (t0: T).(ty3 g c0 (TLRef
123 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
124 (TLRef (plus n h)) (lift n0 O u))) (ty3_abst g (plus n h) c0 d u
125 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) t H1) (plus
126 h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
127 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
128 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
129 (plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
130 d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t:
131 T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
132 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
133 t)))))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3
134 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
135 nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
136 (lift h d t0) (lift h d t3)))))))).(\lambda (c0: C).(\lambda (d:
137 nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
138 (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t4: T).(ty3 g c0
139 t4 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
140 u) (lift h (s (Bind b) d) t3)) (\lambda (t4: T).(ty3 g c0 (THead (Bind b)
141 (lift h d u) (lift h (s (Bind b) d) t0)) t4)) (ty3_bind g c0 (lift h d u)
142 (lift h d t) (H1 c0 d h H4) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
143 c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H4 b u))) (lift h
144 d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) (lift h d (THead
145 (Bind b) u t0)) (lift_head (Bind b) u t0 h d)))))))))))))))) (\lambda (c:
146 C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1:
147 ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
148 (ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda (v: T).(\lambda (t:
149 T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u t))).(\lambda (H3: ((\forall
150 (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0
151 (lift h d v) (lift h d (THead (Bind Abst) u t))))))))).(\lambda (c0:
152 C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0
153 c)).(eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v))
154 (\lambda (t0: T).(ty3 g c0 t0 (lift h d (THead (Flat Appl) w (THead (Bind
155 Abst) u t))))) (eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat
156 Appl) d) (THead (Bind Abst) u t))) (\lambda (t0: T).(ty3 g c0 (THead (Flat
157 Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) t0)) (eq_ind_r T (THead
158 (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s (Flat
159 Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w)
160 (lift h (s (Flat Appl) d) v)) (THead (Flat Appl) (lift h d w) t0))) (ty3_appl
161 g c0 (lift h d w) (lift h d u) (H1 c0 d h H4) (lift h d v) (lift h (S d) t)
162 (eq_ind T (lift h d (THead (Bind Abst) u t)) (\lambda (t0: T).(ty3 g c0 (lift
163 h d v) t0)) (H3 c0 d h H4) (THead (Bind Abst) (lift h d u) (lift h (S d) t))
164 (lift_bind Abst u t h d))) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t))
165 (lift_head (Bind Abst) u t h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
166 w (THead (Bind Abst) u t))) (lift_head (Flat Appl) w (THead (Bind Abst) u t)
167 h d)) (lift h d (THead (Flat Appl) w v)) (lift_head (Flat Appl) w v h
168 d))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda
169 (_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
170 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t0) (lift h d
171 t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3:
172 ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
173 (ty3 g c0 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d:
174 nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
175 (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) (\lambda (t: T).(ty3
176 g c0 t (lift h d (THead (Flat Cast) t4 t3)))) (eq_ind_r T (THead (Flat Cast)
177 (lift h d t4) (lift h (s (Flat Cast) d) t3)) (\lambda (t: T).(ty3 g c0 (THead
178 (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) t)) (ty3_cast g c0
179 (lift h (s (Flat Cast) d) t0) (lift h (s (Flat Cast) d) t3) (H1 c0 (s (Flat
180 Cast) d) h H4) (lift h d t4) (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t4
181 t3)) (lift_head (Flat Cast) t4 t3 h d)) (lift h d (THead (Flat Cast) t3 t0))
182 (lift_head (Flat Cast) t3 t0 h d)))))))))))))) e t1 t2 H))))).
185 \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
186 t1 t2) \to (ex T (\lambda (t: T).(ty3 g c t2 t)))))))
188 \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
189 (H: (ty3 g c t1 t2)).(ty3_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda
190 (t0: T).(ex T (\lambda (t3: T).(ty3 g c0 t0 t3)))))) (\lambda (c0:
191 C).(\lambda (t0: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 t0 t)).(\lambda
192 (_: (ex T (\lambda (t3: T).(ty3 g c0 t t3)))).(\lambda (u: T).(\lambda (t3:
193 T).(\lambda (_: (ty3 g c0 u t3)).(\lambda (_: (ex T (\lambda (t4: T).(ty3 g
194 c0 t3 t4)))).(\lambda (_: (pc3 c0 t3 t0)).(ex_intro T (\lambda (t4: T).(ty3 g
195 c0 t0 t4)) t H0))))))))))) (\lambda (c0: C).(\lambda (m: nat).(ex_intro T
196 (\lambda (t: T).(ty3 g c0 (TSort (next g m)) t)) (TSort (next g (next g m)))
197 (ty3_sort g c0 (next g m))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
198 C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr)
199 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (H2: (ex T (\lambda
200 (t0: T).(ty3 g d t t0)))).(let H3 \def H2 in (ex_ind T (\lambda (t0: T).(ty3
201 g d t t0)) (ex T (\lambda (t0: T).(ty3 g c0 (lift (S n) O t) t0))) (\lambda
202 (x: T).(\lambda (H4: (ty3 g d t x)).(ex_intro T (\lambda (t0: T).(ty3 g c0
203 (lift (S n) O t) t0)) (lift (S n) O x) (ty3_lift g d t x H4 c0 O (S n)
204 (getl_drop Abbr c0 d u n H0))))) H3)))))))))) (\lambda (n: nat).(\lambda (c0:
205 C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind
206 Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (_: (ex T
207 (\lambda (t0: T).(ty3 g d t t0)))).(ex_intro T (\lambda (t0: T).(ty3 g c0
208 (lift (S n) O u) t0)) (lift (S n) O t) (ty3_lift g d u t H1 c0 O (S n)
209 (getl_drop Abst c0 d u n H0))))))))))) (\lambda (c0: C).(\lambda (u:
210 T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: (ex T (\lambda
211 (t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3:
212 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (H3: (ex T
213 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(let H4 \def H3 in
214 (ex_ind T (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)) (ex T
215 (\lambda (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4))) (\lambda (x:
216 T).(\lambda (H5: (ty3 g (CHead c0 (Bind b) u) t3 x)).(ex_intro T (\lambda
217 (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4)) (THead (Bind b) u x) (ty3_bind g
218 c0 u t H0 b t3 x H5)))) H4)))))))))))) (\lambda (c0: C).(\lambda (w:
219 T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T (\lambda
220 (t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g
221 c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: T).(ty3 g c0
222 (THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T (\lambda (t0:
223 T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w
224 (THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_: (ty3 g c0 u
225 x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0 (THead (Bind
226 Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead
227 (Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g c0 (THead (Bind
228 Abst) u t) x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0
229 (THead (Bind Abst) u t3) x0))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u
230 t0))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t
231 t3))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind
232 Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0
233 (THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3 g c0 u x2)).(\lambda (H10:
234 (ty3 g (CHead c0 (Bind Abst) u) t x1)).(ex_intro T (\lambda (t0: T).(ty3 g c0
235 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat Appl) w
236 (THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u t) x1
237 (ty3_bind g c0 u x2 H9 Abst t x1 H10)))))))) (ty3_gen_bind g Abst c0 u t x0
238 H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3:
239 T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g
240 c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 t3 t4)).(\lambda (H3:
241 (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def H3 in (ex_ind T
242 (\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g c0 (THead (Flat
243 Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T
244 (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x
245 t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
248 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
249 t1) \to (\forall (t2: T).((ty3 g c u t2) \to (pc3 c t1 t2)))))))
251 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H:
252 (ty3 g c u t1)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
253 T).(\forall (t2: T).((ty3 g c0 t t2) \to (pc3 c0 t0 t2)))))) (\lambda (c0:
254 C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda
255 (_: ((\forall (t3: T).((ty3 g c0 t2 t3) \to (pc3 c0 t t3))))).(\lambda (u0:
256 T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H3: ((\forall
257 (t3: T).((ty3 g c0 u0 t3) \to (pc3 c0 t0 t3))))).(\lambda (H4: (pc3 c0 t0
258 t2)).(\lambda (t3: T).(\lambda (H5: (ty3 g c0 u0 t3)).(pc3_t t0 c0 t2 (pc3_s
259 c0 t2 t0 H4) t3 (H3 t3 H5)))))))))))))) (\lambda (c0: C).(\lambda (m:
260 nat).(\lambda (t2: T).(\lambda (H0: (ty3 g c0 (TSort m) t2)).(ty3_gen_sort g
261 c0 t2 m H0))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda
262 (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr) u0))).(\lambda (t:
263 T).(\lambda (_: (ty3 g d u0 t)).(\lambda (H2: ((\forall (t2: T).((ty3 g d u0
264 t2) \to (pc3 d t t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n)
265 t2)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
266 T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
267 (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1:
268 T).(\lambda (t0: T).(ty3 g e u1 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
269 (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e:
270 C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u1)))))
271 (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))) (pc3 c0
272 (lift (S n) O t) t2) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_:
273 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
274 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
275 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T
276 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
277 t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e
278 (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g
279 e u1 t0)))) (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1:
280 T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x2) t2)).(\lambda
281 (H6: (getl n c0 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g x0 x1
282 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n
283 c0 c1)) H0 (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n
284 H0 (CHead x0 (Bind Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e:
285 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
286 (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind
287 Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr)
288 x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return
289 (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t0)
290 \Rightarrow t0])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
291 (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
292 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
293 T).(getl n c0 (CHead x0 (Bind Abbr) t0))) H8 u0 H10) in (let H13 \def
294 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
295 (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind Abbr) u0))) H12 d
296 H11) in (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3 g c1 u0 x2)) H13 d
297 H11) in (pc3_t (lift (S n) O x2) c0 (lift (S n) O t) (pc3_lift c0 d (S n) O
298 (getl_drop Abbr c0 d u0 n H14) t x2 (H2 x2 H15)) t2 H5))))))) H9)))))))))
299 H4)) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
300 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
301 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
302 T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_:
303 C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda
304 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst)
305 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))
306 (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
307 T).(\lambda (_: (pc3 c0 (lift (S n) O x1) t2)).(\lambda (H6: (getl n c0
308 (CHead x0 (Bind Abst) x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def
309 (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead
310 x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0
311 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abbr) u0)
312 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
313 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
314 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
315 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
316 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abst)
317 x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abst) x1)
318 H6)) in (False_ind (pc3 c0 (lift (S n) O t) t2) H9))))))))) H4))
319 (ty3_gen_lref g c0 t2 n H3)))))))))))) (\lambda (n: nat).(\lambda (c0:
320 C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind
321 Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_:
322 ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t t2))))).(\lambda (t2:
323 T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(or_ind (ex3_3 C T T (\lambda (_:
324 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
325 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
326 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))
327 (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift
328 (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
329 c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
330 (t0: T).(ty3 g e u1 t0))))) (pc3 c0 (lift (S n) O u0) t2) (\lambda (H4:
331 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift
332 (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
333 c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
334 (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
335 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
336 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
337 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O
338 u0) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3
339 c0 (lift (S n) O x2) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abbr)
340 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind
341 Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abbr) x1)
342 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
343 (let H9 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (ee: C).(match ee in
344 C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k
345 _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
346 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
347 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
348 \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d
349 (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in (False_ind (pc3 c0
350 (lift (S n) O u0) t2) H9))))))))) H4)) (\lambda (H4: (ex3_3 C T T (\lambda
351 (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2))))
352 (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
353 Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1
354 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
355 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
356 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
357 T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O u0) t2) (\lambda
358 (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O
359 x1) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abst) x1))).(\lambda (H7:
360 (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda
361 (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d
362 (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (f_equal
363 C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
364 \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u0)
365 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead
366 x0 (Bind Abst) x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match
367 e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _
368 t0) \Rightarrow t0])) (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
369 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in
370 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
371 T).(getl n c0 (CHead x0 (Bind Abst) t0))) H8 u0 H10) in (let H13 \def
372 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
373 (eq_ind_r T x1 (\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)) H5 u0 H10) in
374 (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind
375 Abst) u0))) H12 d H11) in (let H16 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3
376 g c1 u0 x2)) H13 d H11) in H14))))))) H9))))))))) H4)) (ty3_gen_lref g c0 t2
377 n H3)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t: T).(\lambda
378 (_: (ty3 g c0 u0 t)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 u0 t2) \to
379 (pc3 c0 t t2))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t2: T).(\lambda
380 (_: (ty3 g (CHead c0 (Bind b) u0) t0 t2)).(\lambda (H3: ((\forall (t3:
381 T).((ty3 g (CHead c0 (Bind b) u0) t0 t3) \to (pc3 (CHead c0 (Bind b) u0) t2
382 t3))))).(\lambda (t3: T).(\lambda (H4: (ty3 g c0 (THead (Bind b) u0 t0)
383 t3)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
384 u0 t4) t3))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda
385 (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u0) t0 t4))) (pc3 c0 (THead
386 (Bind b) u0 t2) t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0
387 (THead (Bind b) u0 x0) t3)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H7: (ty3
388 g (CHead c0 (Bind b) u0) t0 x0)).(pc3_t (THead (Bind b) u0 x0) c0 (THead
389 (Bind b) u0 t2) (pc3_head_2 c0 u0 t2 x0 (Bind b) (H3 x0 H7)) t3 H5))))))
390 (ty3_gen_bind g b c0 u0 t0 t3 H4)))))))))))))) (\lambda (c0: C).(\lambda (w:
391 T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2:
392 T).((ty3 g c0 w t2) \to (pc3 c0 u0 t2))))).(\lambda (v: T).(\lambda (t:
393 T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3:
394 ((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0 (THead (Bind Abst) u0 t)
395 t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0 (THead (Flat Appl) w v)
396 t2)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
397 Appl) w (THead (Bind Abst) u1 t0)) t2))) (\lambda (u1: T).(\lambda (t0:
398 T).(ty3 g c0 v (THead (Bind Abst) u1 t0)))) (\lambda (u1: T).(\lambda (_:
399 T).(ty3 g c0 w u1))) (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t))
400 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0 (THead (Flat
401 Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g c0 v (THead
402 (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(pc3_t (THead (Flat Appl)
403 w (THead (Bind Abst) x0 x1)) c0 (THead (Flat Appl) w (THead (Bind Abst) u0
404 t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0 x1) (H3
405 (THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0 w v t2
406 H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: T).(\lambda
407 (_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 t0 t3) \to
408 (pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2 t3)).(\lambda
409 (H3: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 t4))))).(\lambda (t4:
410 T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0) t4)).(ex3_ind T (\lambda
411 (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t0
412 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) (pc3 c0 (THead (Flat Cast) t3 t2) t4)
413 (\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead (Flat Cast) x0 t2)
414 t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g c0 t2 x0)).(pc3_t
415 (THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) (pc3_head_1 c0 t3 x0
416 (H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 t0 t2 t4
417 H4)))))))))))) c u t1 H))))).
419 theorem ty3_gen_abst_abst:
420 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall
421 (t2: T).((ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (ex2
422 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst)
425 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda
426 (t2: T).(\lambda (H: (ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u
427 t2))).(ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) u t2) t)) (ex2 T
428 (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u)
429 t1 t2))) (\lambda (x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2)
430 x)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c (THead (Bind Abst)
431 u t3) x))) (\lambda (_: T).(\lambda (t: T).(ty3 g c u t))) (\lambda (t3:
432 T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t2 t3))) (ex2 T (\lambda
433 (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)))
434 (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c (THead (Bind Abst) u
435 x0) x)).(\lambda (_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c (Bind
436 Abst) u) t2 x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c
437 (THead (Bind Abst) u t3) (THead (Bind Abst) u t2)))) (\lambda (_: T).(\lambda
438 (t: T).(ty3 g c u t))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c (Bind
439 Abst) u) t1 t3))) (ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3
440 g (CHead c (Bind Abst) u) t1 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
441 (H4: (pc3 c (THead (Bind Abst) u x2) (THead (Bind Abst) u t2))).(\lambda (H5:
442 (ty3 g c u x3)).(\lambda (H6: (ty3 g (CHead c (Bind Abst) u) t1 x2)).(let H_y
443 \def (pc3_gen_abst_shift c u x2 t2 H4) in (ex_intro2 T (\lambda (w: T).(ty3 g
444 c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x3 H5
445 (ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x2 H6 H_y))))))))
446 (ty3_gen_bind g Abst c u t1 (THead (Bind Abst) u t2) H))))))) (ty3_gen_bind g
447 Abst c u t2 x H0)))) (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind
448 Abst) u t2) H))))))).
450 theorem ty3_typecheck:
451 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t
452 v) \to (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)))))))
454 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (v: T).(\lambda (H:
455 (ty3 g c t v)).(ex_ind T (\lambda (t0: T).(ty3 g c v t0)) (ex T (\lambda (u:
456 T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g
457 c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u))
458 (THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v
461 theorem ty3_getl_subst0:
462 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
463 u) \to (\forall (v0: T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 t
464 t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c (CHead d
465 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))))
467 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
468 (ty3 g c t u)).(ty3_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (_:
469 T).(\forall (v0: T).(\forall (t2: T).(\forall (i: nat).((subst0 i v0 t0 t2)
470 \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d
471 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda
472 (c0: C).(\lambda (t2: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2
473 t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
474 nat).((subst0 i v0 t2 t1) \to (\forall (b: B).(\forall (d: C).(\forall (v:
475 T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
476 w))))))))))))).(\lambda (u0: T).(\lambda (t1: T).(\lambda (_: (ty3 g c0 u0
477 t1)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i:
478 nat).((subst0 i v0 u0 t3) \to (\forall (b: B).(\forall (d: C).(\forall (v:
479 T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
480 w))))))))))))).(\lambda (_: (pc3 c0 t1 t2)).(\lambda (v0: T).(\lambda (t3:
481 T).(\lambda (i: nat).(\lambda (H5: (subst0 i v0 u0 t3)).(\lambda (b:
482 B).(\lambda (d: C).(\lambda (v: T).(\lambda (H6: (getl i c0 (CHead d (Bind b)
483 v))).(H3 v0 t3 i H5 b d v H6))))))))))))))))))) (\lambda (c0: C).(\lambda (m:
484 nat).(\lambda (v0: T).(\lambda (t0: T).(\lambda (i: nat).(\lambda (H0:
485 (subst0 i v0 (TSort m) t0)).(\lambda (b: B).(\lambda (d: C).(\lambda (v:
486 T).(\lambda (_: (getl i c0 (CHead d (Bind b) v))).(subst0_gen_sort v0 t0 i m
487 H0 (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda (n:
488 nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n
489 c0 (CHead d (Bind Abbr) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0
490 t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i:
491 nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v:
492 T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v
493 w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
494 (H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda
495 (v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(land_ind (eq nat n
496 i) (eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w)))
497 (\lambda (H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7
498 \def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v)))
499 H4 n H5) in (let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1:
500 C).(getl n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
501 Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C
502 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
503 \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0)
504 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0
505 (Bind b) v) H7)) in ((let H10 \def (f_equal C B (\lambda (e: C).(match e in C
506 return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
507 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0)
508 \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u0)
509 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0
510 (Bind b) v) H7)) in ((let H11 \def (f_equal C T (\lambda (e: C).(match e in C
511 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t2)
512 \Rightarrow t2])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) (getl_mono
513 c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12:
514 (eq B Abbr b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v
515 (\lambda (t2: T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T
516 u0 (\lambda (t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def
517 (eq_ind_r C d0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d
518 H13) in (eq_ind C d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w))))
519 (let H16 \def (eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0)
520 u0))) H15 Abbr H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0
521 H13)) v H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n
522 H3)))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
523 C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
524 u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0 t0)).(\lambda (_: ((\forall
525 (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) \to (\forall
526 (b: B).(\forall (d0: C).(\forall (v: T).((getl i d (CHead d0 (Bind b) v)) \to
527 (ex T (\lambda (w: T).(ty3 g d0 v w))))))))))))).(\lambda (v0: T).(\lambda
528 (t1: T).(\lambda (i: nat).(\lambda (H3: (subst0 i v0 (TLRef n) t1)).(\lambda
529 (b: B).(\lambda (d0: C).(\lambda (v: T).(\lambda (H4: (getl i c0 (CHead d0
530 (Bind b) v))).(land_ind (eq nat n i) (eq T t1 (lift (S n) O v0)) (ex T
531 (\lambda (w: T).(ty3 g d0 v w))) (\lambda (H5: (eq nat n i)).(\lambda (_: (eq
532 T t1 (lift (S n) O v0))).(let H7 \def (eq_ind_r nat i (\lambda (n0:
533 nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n H5) in (let H8 \def (eq_ind C
534 (CHead d (Bind Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead d0 (Bind
535 b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7))
536 in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
537 (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1]))
538 (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
539 Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in ((let H10 \def (f_equal C B
540 (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
541 \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k in K return (\lambda
542 (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])]))
543 (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind
544 Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in ((let H11 \def (f_equal C T
545 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
546 \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2])) (CHead d (Bind Abst) u0)
547 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0
548 (Bind b) v) H7)) in (\lambda (H12: (eq B Abst b)).(\lambda (H13: (eq C d
549 d0)).(let H14 \def (eq_ind_r T v (\lambda (t2: T).(getl n c0 (CHead d0 (Bind
550 b) t2))) H8 u0 H11) in (eq_ind T u0 (\lambda (t2: T).(ex T (\lambda (w:
551 T).(ty3 g d0 t2 w)))) (let H15 \def (eq_ind_r C d0 (\lambda (c1: C).(getl n
552 c0 (CHead c1 (Bind b) u0))) H14 d H13) in (eq_ind C d (\lambda (c1: C).(ex T
553 (\lambda (w: T).(ty3 g c1 u0 w)))) (let H16 \def (eq_ind_r B b (\lambda (b0:
554 B).(getl n c0 (CHead d (Bind b0) u0))) H15 Abst H12) in (ex_intro T (\lambda
555 (w: T).(ty3 g d u0 w)) t0 H1)) d0 H13)) v H11))))) H10)) H9))))))
556 (subst0_gen_lref v0 t1 i n H3)))))))))))))))))) (\lambda (c0: C).(\lambda
557 (u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H1:
558 ((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) \to
559 (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b)
560 v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (b:
561 B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b)
562 u0) t1 t2)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i:
563 nat).((subst0 i v0 t1 t3) \to (\forall (b0: B).(\forall (d: C).(\forall (v:
564 T).((getl i (CHead c0 (Bind b) u0) (CHead d (Bind b0) v)) \to (ex T (\lambda
565 (w: T).(ty3 g d v w))))))))))))).(\lambda (v0: T).(\lambda (t3: T).(\lambda
566 (i: nat).(\lambda (H4: (subst0 i v0 (THead (Bind b) u0 t1) t3)).(\lambda (b0:
567 B).(\lambda (d: C).(\lambda (v: T).(\lambda (H5: (getl i c0 (CHead d (Bind
568 b0) v))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1)))
569 (\lambda (u2: T).(subst0 i v0 u0 u2))) (ex2 T (\lambda (t4: T).(eq T t3
570 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))
571 (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2
572 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_:
573 T).(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))) (ex T (\lambda (w:
574 T).(ty3 g d v w))) (\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t3 (THead
575 (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0 u2)))).(ex2_ind T (\lambda
576 (u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0
577 u2)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T
578 t3 (THead (Bind b) x t1))).(\lambda (H8: (subst0 i v0 u0 x)).(H1 v0 x i H8 b0
579 d v H5)))) H6)) (\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind
580 b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))).(ex2_ind T
581 (\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0
582 (s (Bind b) i) v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x:
583 T).(\lambda (_: (eq T t3 (THead (Bind b) u0 x))).(\lambda (H8: (subst0 (s
584 (Bind b) i) v0 t1 x)).(H3 v0 x (S i) H8 b0 d v (getl_head (Bind b) i c0
585 (CHead d (Bind b0) v) H5 u0))))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2:
586 T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2:
587 T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
588 T).(subst0 (s (Bind b) i) v0 t1 t4))))).(ex3_2_ind T T (\lambda (u2:
589 T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2:
590 T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4:
591 T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex T (\lambda (w: T).(ty3 g d v w)))
592 (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t3 (THead (Bind b) x0
593 x1))).(\lambda (H8: (subst0 i v0 u0 x0)).(\lambda (_: (subst0 (s (Bind b) i)
594 v0 t1 x1)).(H1 v0 x0 i H8 b0 d v H5)))))) H6)) (subst0_gen_head (Bind b) v0
595 u0 t1 t3 i H4)))))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda
596 (u0: T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (H1: ((\forall (v0:
597 T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 w t0) \to (\forall (b:
598 B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to (ex
599 T (\lambda (w0: T).(ty3 g d v w0))))))))))))).(\lambda (v: T).(\lambda (t0:
600 T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0 t0))).(\lambda (H3:
601 ((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 v t1) \to
602 (\forall (b: B).(\forall (d: C).(\forall (v1: T).((getl i c0 (CHead d (Bind
603 b) v1)) \to (ex T (\lambda (w0: T).(ty3 g d v1 w0))))))))))))).(\lambda (v0:
604 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat
605 Appl) w v) t1)).(\lambda (b: B).(\lambda (d: C).(\lambda (v1: T).(\lambda
606 (H5: (getl i c0 (CHead d (Bind b) v1))).(or3_ind (ex2 T (\lambda (u2: T).(eq
607 T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w u2))) (ex2 T
608 (\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0
609 (s (Flat Appl) i) v0 v t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq
610 T t1 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i
611 v0 w u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v
612 t2)))) (ex T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (H6: (ex2 T (\lambda
613 (u2: T).(eq T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w
614 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t1 (THead (Flat Appl) u2 v)))
615 (\lambda (u2: T).(subst0 i v0 w u2)) (ex T (\lambda (w0: T).(ty3 g d v1 w0)))
616 (\lambda (x: T).(\lambda (_: (eq T t1 (THead (Flat Appl) x v))).(\lambda (H8:
617 (subst0 i v0 w x)).(H1 v0 x i H8 b d v1 H5)))) H6)) (\lambda (H6: (ex2 T
618 (\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0
619 (s (Flat Appl) i) v0 v t2)))).(ex2_ind T (\lambda (t2: T).(eq T t1 (THead
620 (Flat Appl) w t2))) (\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2)) (ex
621 T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (x: T).(\lambda (_: (eq T t1
622 (THead (Flat Appl) w x))).(\lambda (H8: (subst0 (s (Flat Appl) i) v0 v
623 x)).(H3 v0 x (s (Flat Appl) i) H8 b d v1 H5)))) H6)) (\lambda (H6: (ex3_2 T T
624 (\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2))))
625 (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_:
626 T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))))).(ex3_2_ind T T
627 (\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2))))
628 (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_:
629 T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))) (ex T (\lambda (w0:
630 T).(ty3 g d v1 w0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t1
631 (THead (Flat Appl) x0 x1))).(\lambda (_: (subst0 i v0 w x0)).(\lambda (H9:
632 (subst0 (s (Flat Appl) i) v0 v x1)).(H3 v0 x1 (s (Flat Appl) i) H9 b d v1
633 H5)))))) H6)) (subst0_gen_head (Flat Appl) v0 w v t1 i H4)))))))))))))))))))
634 (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1
635 t2)).(\lambda (H1: ((\forall (v0: T).(\forall (t0: T).(\forall (i:
636 nat).((subst0 i v0 t1 t0) \to (\forall (b: B).(\forall (d: C).(\forall (v:
637 T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v
638 w))))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (H3:
639 ((\forall (v0: T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t2 t3) \to
640 (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b)
641 v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (v0:
642 T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat
643 Cast) t2 t1) t3)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: T).(\lambda
644 (H5: (getl i c0 (CHead d (Bind b) v))).(or3_ind (ex2 T (\lambda (u2: T).(eq T
645 t3 (THead (Flat Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2))) (ex2 T
646 (\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4:
647 T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex3_2 T T (\lambda (u2: T).(\lambda
648 (t4: T).(eq T t3 (THead (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_:
649 T).(subst0 i v0 t2 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat
650 Cast) i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (H6:
651 (ex2 T (\lambda (u2: T).(eq T t3 (THead (Flat Cast) u2 t1))) (\lambda (u2:
652 T).(subst0 i v0 t2 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 (THead (Flat
653 Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2)) (ex T (\lambda (w:
654 T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Flat Cast) x
655 t1))).(\lambda (H8: (subst0 i v0 t2 x)).(H3 v0 x i H8 b d v H5)))) H6))
656 (\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4)))
657 (\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4)))).(ex2_ind T (\lambda
658 (t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4: T).(subst0 (s
659 (Flat Cast) i) v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x:
660 T).(\lambda (_: (eq T t3 (THead (Flat Cast) t2 x))).(\lambda (H8: (subst0 (s
661 (Flat Cast) i) v0 t1 x)).(H1 v0 x (s (Flat Cast) i) H8 b d v H5)))) H6))
662 (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
663 (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2)))
664 (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1
665 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
666 (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2)))
667 (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex T
668 (\lambda (w: T).(ty3 g d v w))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
669 (_: (eq T t3 (THead (Flat Cast) x0 x1))).(\lambda (H8: (subst0 i v0 t2
670 x0)).(\lambda (_: (subst0 (s (Flat Cast) i) v0 t1 x1)).(H3 v0 x0 i H8 b d v
671 H5)))))) H6)) (subst0_gen_head (Flat Cast) v0 t2 t1 t3 i H4))))))))))))))))))
projects / helm.git / blob