1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3".
19 include "csubt/ty3.ma".
21 include "ty3/subst1.ma".
23 include "ty3/fsubst0.ma".
27 include "pc3/wcpr0.ma".
29 include "pc1/props.ma".
31 theorem ty3_sred_wcpr0_pr0:
32 \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1
33 t1 t) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1 t2)
34 \to (ty3 g c2 t2 t)))))))))
36 \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t: T).(\lambda
37 (H: (ty3 g c1 t1 t)).(ty3_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda
38 (t2: T).(\forall (c2: C).((wcpr0 c c2) \to (\forall (t3: T).((pr0 t0 t3) \to
39 (ty3 g c2 t3 t2)))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda (t0:
40 T).(\lambda (_: (ty3 g c t2 t0)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c
41 c2) \to (\forall (t3: T).((pr0 t2 t3) \to (ty3 g c2 t3 t0))))))).(\lambda (u:
42 T).(\lambda (t3: T).(\lambda (_: (ty3 g c u t3)).(\lambda (H3: ((\forall (c2:
43 C).((wcpr0 c c2) \to (\forall (t4: T).((pr0 u t4) \to (ty3 g c2 t4
44 t3))))))).(\lambda (H4: (pc3 c t3 t2)).(\lambda (c2: C).(\lambda (H5: (wcpr0
45 c c2)).(\lambda (t4: T).(\lambda (H6: (pr0 u t4)).(ty3_conv g c2 t2 t0 (H1 c2
46 H5 t2 (pr0_refl t2)) t4 t3 (H3 c2 H5 t4 H6) (pc3_wcpr0 c c2 H5 t3 t2
47 H4)))))))))))))))) (\lambda (c: C).(\lambda (m: nat).(\lambda (c2:
48 C).(\lambda (_: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H1: (pr0 (TSort m)
49 t2)).(eq_ind_r T (TSort m) (\lambda (t0: T).(ty3 g c2 t0 (TSort (next g m))))
50 (ty3_sort g c2 m) t2 (pr0_gen_sort t2 m H1)))))))) (\lambda (n: nat).(\lambda
51 (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind
52 Abbr) u))).(\lambda (t0: T).(\lambda (_: (ty3 g d u t0)).(\lambda (H2:
53 ((\forall (c2: C).((wcpr0 d c2) \to (\forall (t2: T).((pr0 u t2) \to (ty3 g
54 c2 t2 t0))))))).(\lambda (c2: C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2:
55 T).(\lambda (H4: (pr0 (TLRef n) t2)).(eq_ind_r T (TLRef n) (\lambda (t3:
56 T).(ty3 g c2 t3 (lift (S n) O t0))) (ex3_2_ind C T (\lambda (e2: C).(\lambda
57 (u2: T).(getl n c2 (CHead e2 (Bind Abbr) u2)))) (\lambda (e2: C).(\lambda (_:
58 T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u u2))) (ty3 g c2
59 (TLRef n) (lift (S n) O t0)) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5:
60 (getl n c2 (CHead x0 (Bind Abbr) x1))).(\lambda (H6: (wcpr0 d x0)).(\lambda
61 (H7: (pr0 u x1)).(ty3_abbr g n c2 x0 x1 H5 t0 (H2 x0 H6 x1 H7)))))))
62 (wcpr0_getl c c2 H3 n d u (Bind Abbr) H0)) t2 (pr0_gen_lref t2 n
63 H4)))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda
64 (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda (t0:
65 T).(\lambda (_: (ty3 g d u t0)).(\lambda (H2: ((\forall (c2: C).((wcpr0 d c2)
66 \to (\forall (t2: T).((pr0 u t2) \to (ty3 g c2 t2 t0))))))).(\lambda (c2:
67 C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H4: (pr0 (TLRef n)
68 t2)).(eq_ind_r T (TLRef n) (\lambda (t3: T).(ty3 g c2 t3 (lift (S n) O u)))
69 (ex3_2_ind C T (\lambda (e2: C).(\lambda (u2: T).(getl n c2 (CHead e2 (Bind
70 Abst) u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 d e2))) (\lambda (_:
71 C).(\lambda (u2: T).(pr0 u u2))) (ty3 g c2 (TLRef n) (lift (S n) O u))
72 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (getl n c2 (CHead x0 (Bind
73 Abst) x1))).(\lambda (H6: (wcpr0 d x0)).(\lambda (H7: (pr0 u x1)).(ty3_conv g
74 c2 (lift (S n) O u) (lift (S n) O t0) (ty3_lift g x0 u t0 (H2 x0 H6 u
75 (pr0_refl u)) c2 O (S n) (getl_drop Abst c2 x0 x1 n H5)) (TLRef n) (lift (S
76 n) O x1) (ty3_abst g n c2 x0 x1 H5 t0 (H2 x0 H6 x1 H7)) (pc3_lift c2 x0 (S n)
77 O (getl_drop Abst c2 x0 x1 n H5) x1 u (pc3_pr2_x x0 x1 u (pr2_free x0 u x1
78 H7))))))))) (wcpr0_getl c c2 H3 n d u (Bind Abst) H0)) t2 (pr0_gen_lref t2 n
79 H4)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t0: T).(\lambda
80 (_: (ty3 g c u t0)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to
81 (\forall (t2: T).((pr0 u t2) \to (ty3 g c2 t2 t0))))))).(\lambda (b:
82 B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2: (ty3 g (CHead c (Bind b)
83 u) t2 t3)).(\lambda (H3: ((\forall (c2: C).((wcpr0 (CHead c (Bind b) u) c2)
84 \to (\forall (t4: T).((pr0 t2 t4) \to (ty3 g c2 t4 t3))))))).(\lambda (t4:
85 T).(\lambda (H4: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda (H5: ((\forall
86 (c2: C).((wcpr0 (CHead c (Bind b) u) c2) \to (\forall (t5: T).((pr0 t3 t5)
87 \to (ty3 g c2 t5 t4))))))).(\lambda (c2: C).(\lambda (H6: (wcpr0 c
88 c2)).(\lambda (t5: T).(\lambda (H7: (pr0 (THead (Bind b) u t2) t5)).(let H8
89 \def (match H7 in pr0 return (\lambda (t6: T).(\lambda (t7: T).(\lambda (_:
90 (pr0 t6 t7)).((eq T t6 (THead (Bind b) u t2)) \to ((eq T t7 t5) \to (ty3 g c2
91 t5 (THead (Bind b) u t3))))))) with [(pr0_refl t6) \Rightarrow (\lambda (H8:
92 (eq T t6 (THead (Bind b) u t2))).(\lambda (H9: (eq T t6 t5)).(eq_ind T (THead
93 (Bind b) u t2) (\lambda (t7: T).((eq T t7 t5) \to (ty3 g c2 t5 (THead (Bind
94 b) u t3)))) (\lambda (H10: (eq T (THead (Bind b) u t2) t5)).(eq_ind T (THead
95 (Bind b) u t2) (\lambda (t7: T).(ty3 g c2 t7 (THead (Bind b) u t3)))
96 (ty3_bind g c2 u t0 (H1 c2 H6 u (pr0_refl u)) b t2 t3 (H3 (CHead c2 (Bind b)
97 u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t2 (pr0_refl t2)) t4 (H5
98 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t3
99 (pr0_refl t3))) t5 H10)) t6 (sym_eq T t6 (THead (Bind b) u t2) H8) H9))) |
100 (pr0_comp u1 u2 H8 t6 t7 H9 k) \Rightarrow (\lambda (H10: (eq T (THead k u1
101 t6) (THead (Bind b) u t2))).(\lambda (H11: (eq T (THead k u2 t7) t5)).((let
102 H12 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
103 with [(TSort _) \Rightarrow t6 | (TLRef _) \Rightarrow t6 | (THead _ _ t8)
104 \Rightarrow t8])) (THead k u1 t6) (THead (Bind b) u t2) H10) in ((let H13
105 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
106 with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t8 _)
107 \Rightarrow t8])) (THead k u1 t6) (THead (Bind b) u t2) H10) in ((let H14
108 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
109 with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
110 \Rightarrow k0])) (THead k u1 t6) (THead (Bind b) u t2) H10) in (eq_ind K
111 (Bind b) (\lambda (k0: K).((eq T u1 u) \to ((eq T t6 t2) \to ((eq T (THead k0
112 u2 t7) t5) \to ((pr0 u1 u2) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead (Bind b)
113 u t3)))))))) (\lambda (H15: (eq T u1 u)).(eq_ind T u (\lambda (t8: T).((eq T
114 t6 t2) \to ((eq T (THead (Bind b) u2 t7) t5) \to ((pr0 t8 u2) \to ((pr0 t6
115 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))))) (\lambda (H16: (eq T t6
116 t2)).(eq_ind T t2 (\lambda (t8: T).((eq T (THead (Bind b) u2 t7) t5) \to
117 ((pr0 u u2) \to ((pr0 t8 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))))
118 (\lambda (H17: (eq T (THead (Bind b) u2 t7) t5)).(eq_ind T (THead (Bind b) u2
119 t7) (\lambda (t8: T).((pr0 u u2) \to ((pr0 t2 t7) \to (ty3 g c2 t8 (THead
120 (Bind b) u t3))))) (\lambda (H18: (pr0 u u2)).(\lambda (H19: (pr0 t2
121 t7)).(ex_ind T (\lambda (t8: T).(ty3 g (CHead c2 (Bind b) u) t4 t8)) (ty3 g
122 c2 (THead (Bind b) u2 t7) (THead (Bind b) u t3)) (\lambda (x: T).(\lambda
123 (H20: (ty3 g (CHead c2 (Bind b) u) t4 x)).(ex_ind T (\lambda (t8: T).(ty3 g
124 (CHead c2 (Bind b) u2) t3 t8)) (ty3 g c2 (THead (Bind b) u2 t7) (THead (Bind
125 b) u t3)) (\lambda (x0: T).(\lambda (H21: (ty3 g (CHead c2 (Bind b) u2) t3
126 x0)).(ty3_conv g c2 (THead (Bind b) u t3) (THead (Bind b) u t4) (ty3_bind g
127 c2 u t0 (H1 c2 H6 u (pr0_refl u)) b t3 t4 (H5 (CHead c2 (Bind b) u)
128 (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t3 (pr0_refl t3)) x H20)
129 (THead (Bind b) u2 t7) (THead (Bind b) u2 t3) (ty3_bind g c2 u2 t0 (H1 c2 H6
130 u2 H18) b t7 t3 (H3 (CHead c2 (Bind b) u2) (wcpr0_comp c c2 H6 u u2 H18 (Bind
131 b)) t7 H19) x0 H21) (pc3_pr2_x c2 (THead (Bind b) u2 t3) (THead (Bind b) u
132 t3) (pr2_head_1 c2 u u2 (pr2_free c2 u u2 H18) (Bind b) t3))))) (ty3_correct
133 g (CHead c2 (Bind b) u2) t7 t3 (H3 (CHead c2 (Bind b) u2) (wcpr0_comp c c2 H6
134 u u2 H18 (Bind b)) t7 H19))))) (ty3_correct g (CHead c2 (Bind b) u) t3 t4 (H5
135 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t3
136 (pr0_refl t3)))))) t5 H17)) t6 (sym_eq T t6 t2 H16))) u1 (sym_eq T u1 u
137 H15))) k (sym_eq K k (Bind b) H14))) H13)) H12)) H11 H8 H9))) | (pr0_beta u0
138 v1 v2 H8 t6 t7 H9) \Rightarrow (\lambda (H10: (eq T (THead (Flat Appl) v1
139 (THead (Bind Abst) u0 t6)) (THead (Bind b) u t2))).(\lambda (H11: (eq T
140 (THead (Bind Abbr) v2 t7) t5)).((let H12 \def (eq_ind T (THead (Flat Appl) v1
141 (THead (Bind Abst) u0 t6)) (\lambda (e: T).(match e in T return (\lambda (_:
142 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
143 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
144 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind
145 b) u t2) H10) in (False_ind ((eq T (THead (Bind Abbr) v2 t7) t5) \to ((pr0 v1
146 v2) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))) H12)) H11 H8
147 H9))) | (pr0_upsilon b0 H8 v1 v2 H9 u1 u2 H10 t6 t7 H11) \Rightarrow (\lambda
148 (H12: (eq T (THead (Flat Appl) v1 (THead (Bind b0) u1 t6)) (THead (Bind b) u
149 t2))).(\lambda (H13: (eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O)
150 O v2) t7)) t5)).((let H14 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind
151 b0) u1 t6)) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
152 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
153 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
154 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t2)
155 H12) in (False_ind ((eq T (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O)
156 O v2) t7)) t5) \to ((not (eq B b0 Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2)
157 \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))))) H14)) H13 H8 H9
158 H10 H11))) | (pr0_delta u1 u2 H8 t6 t7 H9 w H10) \Rightarrow (\lambda (H11:
159 (eq T (THead (Bind Abbr) u1 t6) (THead (Bind b) u t2))).(\lambda (H12: (eq T
160 (THead (Bind Abbr) u2 w) t5)).((let H13 \def (f_equal T T (\lambda (e:
161 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t6 |
162 (TLRef _) \Rightarrow t6 | (THead _ _ t8) \Rightarrow t8])) (THead (Bind
163 Abbr) u1 t6) (THead (Bind b) u t2) H11) in ((let H14 \def (f_equal T T
164 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
165 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t8 _) \Rightarrow t8]))
166 (THead (Bind Abbr) u1 t6) (THead (Bind b) u t2) H11) in ((let H15 \def
167 (f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with
168 [(TSort _) \Rightarrow Abbr | (TLRef _) \Rightarrow Abbr | (THead k _ _)
169 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0)
170 \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (THead (Bind Abbr) u1 t6)
171 (THead (Bind b) u t2) H11) in (eq_ind B Abbr (\lambda (b0: B).((eq T u1 u)
172 \to ((eq T t6 t2) \to ((eq T (THead (Bind Abbr) u2 w) t5) \to ((pr0 u1 u2)
173 \to ((pr0 t6 t7) \to ((subst0 O u2 t7 w) \to (ty3 g c2 t5 (THead (Bind b0) u
174 t3))))))))) (\lambda (H16: (eq T u1 u)).(eq_ind T u (\lambda (t8: T).((eq T
175 t6 t2) \to ((eq T (THead (Bind Abbr) u2 w) t5) \to ((pr0 t8 u2) \to ((pr0 t6
176 t7) \to ((subst0 O u2 t7 w) \to (ty3 g c2 t5 (THead (Bind Abbr) u t3))))))))
177 (\lambda (H17: (eq T t6 t2)).(eq_ind T t2 (\lambda (t8: T).((eq T (THead
178 (Bind Abbr) u2 w) t5) \to ((pr0 u u2) \to ((pr0 t8 t7) \to ((subst0 O u2 t7
179 w) \to (ty3 g c2 t5 (THead (Bind Abbr) u t3))))))) (\lambda (H18: (eq T
180 (THead (Bind Abbr) u2 w) t5)).(eq_ind T (THead (Bind Abbr) u2 w) (\lambda
181 (t8: T).((pr0 u u2) \to ((pr0 t2 t7) \to ((subst0 O u2 t7 w) \to (ty3 g c2 t8
182 (THead (Bind Abbr) u t3)))))) (\lambda (H19: (pr0 u u2)).(\lambda (H20: (pr0
183 t2 t7)).(\lambda (H21: (subst0 O u2 t7 w)).(let H22 \def (eq_ind_r B b
184 (\lambda (b0: B).(\forall (c3: C).((wcpr0 (CHead c (Bind b0) u) c3) \to
185 (\forall (t8: T).((pr0 t3 t8) \to (ty3 g c3 t8 t4)))))) H5 Abbr H15) in (let
186 H23 \def (eq_ind_r B b (\lambda (b0: B).(ty3 g (CHead c (Bind b0) u) t3 t4))
187 H4 Abbr H15) in (let H24 \def (eq_ind_r B b (\lambda (b0: B).(\forall (c3:
188 C).((wcpr0 (CHead c (Bind b0) u) c3) \to (\forall (t8: T).((pr0 t2 t8) \to
189 (ty3 g c3 t8 t3)))))) H3 Abbr H15) in (let H25 \def (eq_ind_r B b (\lambda
190 (b0: B).(ty3 g (CHead c (Bind b0) u) t2 t3)) H2 Abbr H15) in (ex_ind T
191 (\lambda (t8: T).(ty3 g (CHead c2 (Bind Abbr) u) t4 t8)) (ty3 g c2 (THead
192 (Bind Abbr) u2 w) (THead (Bind Abbr) u t3)) (\lambda (x: T).(\lambda (H26:
193 (ty3 g (CHead c2 (Bind Abbr) u) t4 x)).(ex_ind T (\lambda (t8: T).(ty3 g
194 (CHead c2 (Bind Abbr) u2) t3 t8)) (ty3 g c2 (THead (Bind Abbr) u2 w) (THead
195 (Bind Abbr) u t3)) (\lambda (x0: T).(\lambda (H27: (ty3 g (CHead c2 (Bind
196 Abbr) u2) t3 x0)).(ty3_conv g c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr)
197 u t4) (ty3_bind g c2 u t0 (H1 c2 H6 u (pr0_refl u)) Abbr t3 t4 (H22 (CHead c2
198 (Bind Abbr) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind Abbr)) t3 (pr0_refl
199 t3)) x H26) (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u2 t3) (ty3_bind g c2
200 u2 t0 (H1 c2 H6 u2 H19) Abbr w t3 (ty3_subst0 g (CHead c2 (Bind Abbr) u2) t7
201 t3 (H24 (CHead c2 (Bind Abbr) u2) (wcpr0_comp c c2 H6 u u2 H19 (Bind Abbr))
202 t7 H20) c2 u2 O (getl_refl Abbr c2 u2) w H21) x0 H27) (pc3_pr2_x c2 (THead
203 (Bind Abbr) u2 t3) (THead (Bind Abbr) u t3) (pr2_head_1 c2 u u2 (pr2_free c2
204 u u2 H19) (Bind Abbr) t3))))) (ty3_correct g (CHead c2 (Bind Abbr) u2) t7 t3
205 (H24 (CHead c2 (Bind Abbr) u2) (wcpr0_comp c c2 H6 u u2 H19 (Bind Abbr)) t7
206 H20))))) (ty3_correct g (CHead c2 (Bind Abbr) u) t3 t4 (H22 (CHead c2 (Bind
207 Abbr) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind Abbr)) t3 (pr0_refl
208 t3))))))))))) t5 H18)) t6 (sym_eq T t6 t2 H17))) u1 (sym_eq T u1 u H16))) b
209 H15)) H14)) H13)) H12 H8 H9 H10))) | (pr0_zeta b0 H8 t6 t7 H9 u0) \Rightarrow
210 (\lambda (H10: (eq T (THead (Bind b0) u0 (lift (S O) O t6)) (THead (Bind b) u
211 t2))).(\lambda (H11: (eq T t7 t5)).((let H12 \def (f_equal T T (\lambda (e:
212 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let
213 rec lref_map (f: ((nat \to nat))) (d: nat) (t8: T) on t8: T \def (match t8
214 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match
215 (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u1
216 t9) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) t9))]) in
217 lref_map) (\lambda (x: nat).(plus x (S O))) O t6) | (TLRef _) \Rightarrow
218 ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t8: T) on t8: T \def (match
219 t8 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef
220 (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) |
221 (THead k u1 t9) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d)
222 t9))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O t6) | (THead _ _ t8)
223 \Rightarrow t8])) (THead (Bind b0) u0 (lift (S O) O t6)) (THead (Bind b) u
224 t2) H10) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e in T return
225 (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0
226 | (THead _ t8 _) \Rightarrow t8])) (THead (Bind b0) u0 (lift (S O) O t6))
227 (THead (Bind b) u t2) H10) in ((let H14 \def (f_equal T B (\lambda (e:
228 T).(match e in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b0 |
229 (TLRef _) \Rightarrow b0 | (THead k _ _) \Rightarrow (match k in K return
230 (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow
231 b0])])) (THead (Bind b0) u0 (lift (S O) O t6)) (THead (Bind b) u t2) H10) in
232 (eq_ind B b (\lambda (b1: B).((eq T u0 u) \to ((eq T (lift (S O) O t6) t2)
233 \to ((eq T t7 t5) \to ((not (eq B b1 Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5
234 (THead (Bind b) u t3)))))))) (\lambda (H15: (eq T u0 u)).(eq_ind T u (\lambda
235 (_: T).((eq T (lift (S O) O t6) t2) \to ((eq T t7 t5) \to ((not (eq B b
236 Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))))) (\lambda
237 (H16: (eq T (lift (S O) O t6) t2)).(eq_ind T (lift (S O) O t6) (\lambda (_:
238 T).((eq T t7 t5) \to ((not (eq B b Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5
239 (THead (Bind b) u t3)))))) (\lambda (H17: (eq T t7 t5)).(eq_ind T t5 (\lambda
240 (t8: T).((not (eq B b Abst)) \to ((pr0 t6 t8) \to (ty3 g c2 t5 (THead (Bind
241 b) u t3))))) (\lambda (H18: (not (eq B b Abst))).(\lambda (H19: (pr0 t6
242 t5)).(let H20 \def (eq_ind_r T t2 (\lambda (t8: T).(\forall (c3: C).((wcpr0
243 (CHead c (Bind b) u) c3) \to (\forall (t9: T).((pr0 t8 t9) \to (ty3 g c3 t9
244 t3)))))) H3 (lift (S O) O t6) H16) in (let H21 \def (eq_ind_r T t2 (\lambda
245 (t8: T).(ty3 g (CHead c (Bind b) u) t8 t3)) H2 (lift (S O) O t6) H16) in
246 (ex_ind T (\lambda (t8: T).(ty3 g (CHead c2 (Bind b) u) t4 t8)) (ty3 g c2 t5
247 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H22: (ty3 g (CHead c2 (Bind
248 b) u) t4 x)).(B_ind (\lambda (b1: B).((not (eq B b1 Abst)) \to ((ty3 g (CHead
249 c2 (Bind b1) u) t3 t4) \to ((ty3 g (CHead c2 (Bind b1) u) t4 x) \to ((ty3 g
250 (CHead c2 (Bind b1) u) (lift (S O) O t5) t3) \to (ty3 g c2 t5 (THead (Bind
251 b1) u t3))))))) (\lambda (H23: (not (eq B Abbr Abst))).(\lambda (H24: (ty3 g
252 (CHead c2 (Bind Abbr) u) t3 t4)).(\lambda (H25: (ty3 g (CHead c2 (Bind Abbr)
253 u) t4 x)).(\lambda (H26: (ty3 g (CHead c2 (Bind Abbr) u) (lift (S O) O t5)
254 t3)).(let H27 \def (ty3_gen_cabbr g (CHead c2 (Bind Abbr) u) (lift (S O) O
255 t5) t3 H26 c2 u O (getl_refl Abbr c2 u) (CHead c2 (Bind Abbr) u)
256 (csubst1_refl O u (CHead c2 (Bind Abbr) u)) c2 (drop_drop (Bind Abbr) O c2 c2
257 (drop_refl c2) u)) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1
258 O u (lift (S O) O t5) (lift (S O) O y1)))) (\lambda (_: T).(\lambda (y2:
259 T).(subst1 O u t3 (lift (S O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
260 g c2 y1 y2))) (ty3 g c2 t5 (THead (Bind Abbr) u t3)) (\lambda (x0:
261 T).(\lambda (x1: T).(\lambda (H28: (subst1 O u (lift (S O) O t5) (lift (S O)
262 O x0))).(\lambda (H29: (subst1 O u t3 (lift (S O) O x1))).(\lambda (H30: (ty3
263 g c2 x0 x1)).(let H31 \def (eq_ind T x0 (\lambda (t8: T).(ty3 g c2 t8 x1))
264 H30 t5 (lift_inj x0 t5 (S O) O (subst1_gen_lift_eq t5 u (lift (S O) O x0) (S
265 O) O O (le_n O) (eq_ind_r nat (plus (S O) O) (\lambda (n: nat).(lt O n))
266 (le_n (plus (S O) O)) (plus O (S O)) (plus_comm O (S O))) H28))) in (ty3_conv
267 g c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t4) (ty3_bind g c2 u t0
268 (H1 c2 H6 u (pr0_refl u)) Abbr t3 t4 H24 x H25) t5 x1 H31 (pc3_pr3_x c2 x1
269 (THead (Bind Abbr) u t3) (pr3_t (THead (Bind Abbr) u (lift (S O) O x1))
270 (THead (Bind Abbr) u t3) c2 (pr3_pr2 c2 (THead (Bind Abbr) u t3) (THead (Bind
271 Abbr) u (lift (S O) O x1)) (pr2_free c2 (THead (Bind Abbr) u t3) (THead (Bind
272 Abbr) u (lift (S O) O x1)) (pr0_delta1 u u (pr0_refl u) t3 t3 (pr0_refl t3)
273 (lift (S O) O x1) H29))) x1 (pr3_pr2 c2 (THead (Bind Abbr) u (lift (S O) O
274 x1)) x1 (pr2_free c2 (THead (Bind Abbr) u (lift (S O) O x1)) x1 (pr0_zeta
275 Abbr H23 x1 x1 (pr0_refl x1) u)))))))))))) H27)))))) (\lambda (H23: (not (eq
276 B Abst Abst))).(\lambda (_: (ty3 g (CHead c2 (Bind Abst) u) t3 t4)).(\lambda
277 (_: (ty3 g (CHead c2 (Bind Abst) u) t4 x)).(\lambda (_: (ty3 g (CHead c2
278 (Bind Abst) u) (lift (S O) O t5) t3)).(let H27 \def (match (H23 (refl_equal B
279 Abst)) in False return (\lambda (_: False).(ty3 g c2 t5 (THead (Bind Abst) u
280 t3))) with []) in H27))))) (\lambda (H23: (not (eq B Void Abst))).(\lambda
281 (H24: (ty3 g (CHead c2 (Bind Void) u) t3 t4)).(\lambda (H25: (ty3 g (CHead c2
282 (Bind Void) u) t4 x)).(\lambda (H26: (ty3 g (CHead c2 (Bind Void) u) (lift (S
283 O) O t5) t3)).(let H27 \def (ty3_gen_cvoid g (CHead c2 (Bind Void) u) (lift
284 (S O) O t5) t3 H26 c2 u O (getl_refl Void c2 u) c2 (drop_drop (Bind Void) O
285 c2 c2 (drop_refl c2) u)) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_:
286 T).(eq T (lift (S O) O t5) (lift (S O) O y1)))) (\lambda (_: T).(\lambda (y2:
287 T).(eq T t3 (lift (S O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g c2
288 y1 y2))) (ty3 g c2 t5 (THead (Bind Void) u t3)) (\lambda (x0: T).(\lambda
289 (x1: T).(\lambda (H28: (eq T (lift (S O) O t5) (lift (S O) O x0))).(\lambda
290 (H29: (eq T t3 (lift (S O) O x1))).(\lambda (H30: (ty3 g c2 x0 x1)).(let H31
291 \def (eq_ind T t3 (\lambda (t8: T).(ty3 g (CHead c2 (Bind Void) u) t8 t4))
292 H24 (lift (S O) O x1) H29) in (eq_ind_r T (lift (S O) O x1) (\lambda (t8:
293 T).(ty3 g c2 t5 (THead (Bind Void) u t8))) (let H32 \def (eq_ind_r T x0
294 (\lambda (t8: T).(ty3 g c2 t8 x1)) H30 t5 (lift_inj t5 x0 (S O) O H28)) in
295 (ty3_conv g c2 (THead (Bind Void) u (lift (S O) O x1)) (THead (Bind Void) u
296 t4) (ty3_bind g c2 u t0 (H1 c2 H6 u (pr0_refl u)) Void (lift (S O) O x1) t4
297 H31 x H25) t5 x1 H32 (pc3_s c2 x1 (THead (Bind Void) u (lift (S O) O x1))
298 (pc3_pr2_r c2 (THead (Bind Void) u (lift (S O) O x1)) x1 (pr2_free c2 (THead
299 (Bind Void) u (lift (S O) O x1)) x1 (pr0_zeta Void H23 x1 x1 (pr0_refl x1)
300 u)))))) t3 H29))))))) H27)))))) b H18 (H5 (CHead c2 (Bind b) u) (wcpr0_comp c
301 c2 H6 u u (pr0_refl u) (Bind b)) t3 (pr0_refl t3)) H22 (H20 (CHead c2 (Bind
302 b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) (lift (S O) O t5)
303 (pr0_lift t6 t5 H19 (S O) O))))) (ty3_correct g (CHead c2 (Bind b) u) t3 t4
304 (H5 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t3
305 (pr0_refl t3)))))))) t7 (sym_eq T t7 t5 H17))) t2 H16)) u0 (sym_eq T u0 u
306 H15))) b0 (sym_eq B b0 b H14))) H13)) H12)) H11 H8 H9))) | (pr0_epsilon t6 t7
307 H8 u0) \Rightarrow (\lambda (H9: (eq T (THead (Flat Cast) u0 t6) (THead (Bind
308 b) u t2))).(\lambda (H10: (eq T t7 t5)).((let H11 \def (eq_ind T (THead (Flat
309 Cast) u0 t6) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
310 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
311 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
312 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t2)
313 H9) in (False_ind ((eq T t7 t5) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead
314 (Bind b) u t3)))) H11)) H10 H8)))]) in (H8 (refl_equal T (THead (Bind b) u
315 t2)) (refl_equal T t5)))))))))))))))))))) (\lambda (c: C).(\lambda (w:
316 T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2:
317 C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 w t2) \to (ty3 g c2 t2
318 u))))))).(\lambda (v: T).(\lambda (t0: T).(\lambda (H2: (ty3 g c v (THead
319 (Bind Abst) u t0))).(\lambda (H3: ((\forall (c2: C).((wcpr0 c c2) \to
320 (\forall (t2: T).((pr0 v t2) \to (ty3 g c2 t2 (THead (Bind Abst) u
321 t0)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2:
322 T).(\lambda (H5: (pr0 (THead (Flat Appl) w v) t2)).(let H6 \def (match H5 in
323 pr0 return (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).((eq T
324 t3 (THead (Flat Appl) w v)) \to ((eq T t4 t2) \to (ty3 g c2 t2 (THead (Flat
325 Appl) w (THead (Bind Abst) u t0)))))))) with [(pr0_refl t3) \Rightarrow
326 (\lambda (H6: (eq T t3 (THead (Flat Appl) w v))).(\lambda (H7: (eq T t3
327 t2)).(eq_ind T (THead (Flat Appl) w v) (\lambda (t4: T).((eq T t4 t2) \to
328 (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))) (\lambda (H8:
329 (eq T (THead (Flat Appl) w v) t2)).(eq_ind T (THead (Flat Appl) w v) (\lambda
330 (t4: T).(ty3 g c2 t4 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
331 (ty3_appl g c2 w u (H1 c2 H4 w (pr0_refl w)) v t0 (H3 c2 H4 v (pr0_refl v)))
332 t2 H8)) t3 (sym_eq T t3 (THead (Flat Appl) w v) H6) H7))) | (pr0_comp u1 u2
333 H6 t3 t4 H7 k) \Rightarrow (\lambda (H8: (eq T (THead k u1 t3) (THead (Flat
334 Appl) w v))).(\lambda (H9: (eq T (THead k u2 t4) t2)).((let H10 \def (f_equal
335 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
336 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t5) \Rightarrow t5]))
337 (THead k u1 t3) (THead (Flat Appl) w v) H8) in ((let H11 \def (f_equal T T
338 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
339 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t5 _) \Rightarrow t5]))
340 (THead k u1 t3) (THead (Flat Appl) w v) H8) in ((let H12 \def (f_equal T K
341 (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
342 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0]))
343 (THead k u1 t3) (THead (Flat Appl) w v) H8) in (eq_ind K (Flat Appl) (\lambda
344 (k0: K).((eq T u1 w) \to ((eq T t3 v) \to ((eq T (THead k0 u2 t4) t2) \to
345 ((pr0 u1 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead
346 (Bind Abst) u t0))))))))) (\lambda (H13: (eq T u1 w)).(eq_ind T w (\lambda
347 (t5: T).((eq T t3 v) \to ((eq T (THead (Flat Appl) u2 t4) t2) \to ((pr0 t5
348 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst)
349 u t0)))))))) (\lambda (H14: (eq T t3 v)).(eq_ind T v (\lambda (t5: T).((eq T
350 (THead (Flat Appl) u2 t4) t2) \to ((pr0 w u2) \to ((pr0 t5 t4) \to (ty3 g c2
351 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))) (\lambda (H15: (eq T
352 (THead (Flat Appl) u2 t4) t2)).(eq_ind T (THead (Flat Appl) u2 t4) (\lambda
353 (t5: T).((pr0 w u2) \to ((pr0 v t4) \to (ty3 g c2 t5 (THead (Flat Appl) w
354 (THead (Bind Abst) u t0)))))) (\lambda (H16: (pr0 w u2)).(\lambda (H17: (pr0
355 v t4)).(ex_ind T (\lambda (t5: T).(ty3 g c2 (THead (Bind Abst) u t0) t5))
356 (ty3 g c2 (THead (Flat Appl) u2 t4) (THead (Flat Appl) w (THead (Bind Abst) u
357 t0))) (\lambda (x: T).(\lambda (H18: (ty3 g c2 (THead (Bind Abst) u t0)
358 x)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c2
359 (THead (Bind Abst) u t5) x)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_:
360 T).(ty3 g c2 u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
361 (CHead c2 (Bind Abst) u) t0 t5)))) (\lambda (t5: T).(\lambda (_: T).(\lambda
362 (t7: T).(ty3 g (CHead c2 (Bind Abst) u) t5 t7)))) (ty3 g c2 (THead (Flat
363 Appl) u2 t4) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x0:
364 T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c2 (THead (Bind Abst)
365 u x0) x)).(\lambda (H20: (ty3 g c2 u x1)).(\lambda (H21: (ty3 g (CHead c2
366 (Bind Abst) u) t0 x0)).(\lambda (H22: (ty3 g (CHead c2 (Bind Abst) u) x0
367 x2)).(ty3_conv g c2 (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead
368 (Flat Appl) w (THead (Bind Abst) u x0)) (ty3_appl g c2 w u (H1 c2 H4 w
369 (pr0_refl w)) (THead (Bind Abst) u t0) x0 (ty3_bind g c2 u x1 H20 Abst t0 x0
370 H21 x2 H22)) (THead (Flat Appl) u2 t4) (THead (Flat Appl) u2 (THead (Bind
371 Abst) u t0)) (ty3_appl g c2 u2 u (H1 c2 H4 u2 H16) t4 t0 (H3 c2 H4 t4 H17))
372 (pc3_pr2_x c2 (THead (Flat Appl) u2 (THead (Bind Abst) u t0)) (THead (Flat
373 Appl) w (THead (Bind Abst) u t0)) (pr2_head_1 c2 w u2 (pr2_free c2 w u2 H16)
374 (Flat Appl) (THead (Bind Abst) u t0))))))))))) (ty3_gen_bind g Abst c2 u t0 x
375 H18)))) (ty3_correct g c2 v (THead (Bind Abst) u t0) (H3 c2 H4 v (pr0_refl
376 v)))))) t2 H15)) t3 (sym_eq T t3 v H14))) u1 (sym_eq T u1 w H13))) k (sym_eq
377 K k (Flat Appl) H12))) H11)) H10)) H9 H6 H7))) | (pr0_beta u0 v1 v2 H6 t3 t4
378 H7) \Rightarrow (\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind Abst)
379 u0 t3)) (THead (Flat Appl) w v))).(\lambda (H9: (eq T (THead (Bind Abbr) v2
380 t4) t2)).((let H10 \def (f_equal T T (\lambda (e: T).(match e in T return
381 (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead (Bind Abst) u0 t3) |
382 (TLRef _) \Rightarrow (THead (Bind Abst) u0 t3) | (THead _ _ t5) \Rightarrow
383 t5])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) w
384 v) H8) in ((let H11 \def (f_equal T T (\lambda (e: T).(match e in T return
385 (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1
386 | (THead _ t5 _) \Rightarrow t5])) (THead (Flat Appl) v1 (THead (Bind Abst)
387 u0 t3)) (THead (Flat Appl) w v) H8) in (eq_ind T w (\lambda (t5: T).((eq T
388 (THead (Bind Abst) u0 t3) v) \to ((eq T (THead (Bind Abbr) v2 t4) t2) \to
389 ((pr0 t5 v2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead
390 (Bind Abst) u t0)))))))) (\lambda (H12: (eq T (THead (Bind Abst) u0 t3)
391 v)).(eq_ind T (THead (Bind Abst) u0 t3) (\lambda (_: T).((eq T (THead (Bind
392 Abbr) v2 t4) t2) \to ((pr0 w v2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead
393 (Flat Appl) w (THead (Bind Abst) u t0))))))) (\lambda (H13: (eq T (THead
394 (Bind Abbr) v2 t4) t2)).(eq_ind T (THead (Bind Abbr) v2 t4) (\lambda (t5:
395 T).((pr0 w v2) \to ((pr0 t3 t4) \to (ty3 g c2 t5 (THead (Flat Appl) w (THead
396 (Bind Abst) u t0)))))) (\lambda (H14: (pr0 w v2)).(\lambda (H15: (pr0 t3
397 t4)).(let H16 \def (eq_ind_r T v (\lambda (t5: T).(\forall (c3: C).((wcpr0 c
398 c3) \to (\forall (t6: T).((pr0 t5 t6) \to (ty3 g c3 t6 (THead (Bind Abst) u
399 t0))))))) H3 (THead (Bind Abst) u0 t3) H12) in (let H17 \def (eq_ind_r T v
400 (\lambda (t5: T).(ty3 g c t5 (THead (Bind Abst) u t0))) H2 (THead (Bind Abst)
401 u0 t3) H12) in (ex_ind T (\lambda (t5: T).(ty3 g c2 (THead (Bind Abst) u t0)
402 t5)) (ty3 g c2 (THead (Bind Abbr) v2 t4) (THead (Flat Appl) w (THead (Bind
403 Abst) u t0))) (\lambda (x: T).(\lambda (H18: (ty3 g c2 (THead (Bind Abst) u
404 t0) x)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
405 T).(pc3 c2 (THead (Bind Abst) u t5) x)))) (\lambda (_: T).(\lambda (t6:
406 T).(\lambda (_: T).(ty3 g c2 u t6)))) (\lambda (t5: T).(\lambda (_:
407 T).(\lambda (_: T).(ty3 g (CHead c2 (Bind Abst) u) t0 t5)))) (\lambda (t5:
408 T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c2 (Bind Abst) u) t5 t7))))
409 (ty3 g c2 (THead (Bind Abbr) v2 t4) (THead (Flat Appl) w (THead (Bind Abst) u
410 t0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c2
411 (THead (Bind Abst) u x0) x)).(\lambda (H20: (ty3 g c2 u x1)).(\lambda (H21:
412 (ty3 g (CHead c2 (Bind Abst) u) t0 x0)).(\lambda (H22: (ty3 g (CHead c2 (Bind
413 Abst) u) x0 x2)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda
414 (_: T).(pc3 c2 (THead (Bind Abst) u0 t5) (THead (Bind Abst) u t0)))))
415 (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c2 u0 t6)))) (\lambda
416 (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind Abst) u0) t4
417 t5)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c2
418 (Bind Abst) u0) t5 t7)))) (ty3 g c2 (THead (Bind Abbr) v2 t4) (THead (Flat
419 Appl) w (THead (Bind Abst) u t0))) (\lambda (x3: T).(\lambda (x4: T).(\lambda
420 (x5: T).(\lambda (H23: (pc3 c2 (THead (Bind Abst) u0 x3) (THead (Bind Abst) u
421 t0))).(\lambda (H24: (ty3 g c2 u0 x4)).(\lambda (H25: (ty3 g (CHead c2 (Bind
422 Abst) u0) t4 x3)).(\lambda (H26: (ty3 g (CHead c2 (Bind Abst) u0) x3
423 x5)).(and_ind (pc3 c2 u0 u) (\forall (b: B).(\forall (u1: T).(pc3 (CHead c2
424 (Bind b) u1) x3 t0))) (ty3 g c2 (THead (Bind Abbr) v2 t4) (THead (Flat Appl)
425 w (THead (Bind Abst) u t0))) (\lambda (H27: (pc3 c2 u0 u)).(\lambda (H28:
426 ((\forall (b: B).(\forall (u1: T).(pc3 (CHead c2 (Bind b) u1) x3
427 t0))))).(ty3_conv g c2 (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead
428 (Flat Appl) w (THead (Bind Abst) u x0)) (ty3_appl g c2 w u (H1 c2 H4 w
429 (pr0_refl w)) (THead (Bind Abst) u t0) x0 (ty3_bind g c2 u x1 H20 Abst t0 x0
430 H21 x2 H22)) (THead (Bind Abbr) v2 t4) (THead (Bind Abbr) v2 x3) (ty3_bind g
431 c2 v2 u (H1 c2 H4 v2 H14) Abbr t4 x3 (csubt_ty3_ld g c2 v2 u0 (ty3_conv g c2
432 u0 x4 H24 v2 u (H1 c2 H4 v2 H14) (pc3_s c2 u u0 H27)) t4 x3 H25) x5
433 (csubt_ty3_ld g c2 v2 u0 (ty3_conv g c2 u0 x4 H24 v2 u (H1 c2 H4 v2 H14)
434 (pc3_s c2 u u0 H27)) x3 x5 H26)) (pc3_t (THead (Bind Abbr) v2 t0) c2 (THead
435 (Bind Abbr) v2 x3) (pc3_head_2 c2 v2 x3 t0 (Bind Abbr) (H28 Abbr v2)) (THead
436 (Flat Appl) w (THead (Bind Abst) u t0)) (pc3_pr2_x c2 (THead (Bind Abbr) v2
437 t0) (THead (Flat Appl) w (THead (Bind Abst) u t0)) (pr2_free c2 (THead (Flat
438 Appl) w (THead (Bind Abst) u t0)) (THead (Bind Abbr) v2 t0) (pr0_beta u w v2
439 H14 t0 t0 (pr0_refl t0)))))))) (pc3_gen_abst c2 u0 u x3 t0 H23)))))))))
440 (ty3_gen_bind g Abst c2 u0 t4 (THead (Bind Abst) u t0) (H16 c2 H4 (THead
441 (Bind Abst) u0 t4) (pr0_comp u0 u0 (pr0_refl u0) t3 t4 H15 (Bind
442 Abst)))))))))))) (ty3_gen_bind g Abst c2 u t0 x H18)))) (ty3_correct g c2
443 (THead (Bind Abst) u0 t3) (THead (Bind Abst) u t0) (H16 c2 H4 (THead (Bind
444 Abst) u0 t3) (pr0_refl (THead (Bind Abst) u0 t3))))))))) t2 H13)) v H12)) v1
445 (sym_eq T v1 w H11))) H10)) H9 H6 H7))) | (pr0_upsilon b H6 v1 v2 H7 u1 u2 H8
446 t3 t4 H9) \Rightarrow (\lambda (H10: (eq T (THead (Flat Appl) v1 (THead (Bind
447 b) u1 t3)) (THead (Flat Appl) w v))).(\lambda (H11: (eq T (THead (Bind b) u2
448 (THead (Flat Appl) (lift (S O) O v2) t4)) t2)).((let H12 \def (f_equal T T
449 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
450 \Rightarrow (THead (Bind b) u1 t3) | (TLRef _) \Rightarrow (THead (Bind b) u1
451 t3) | (THead _ _ t5) \Rightarrow t5])) (THead (Flat Appl) v1 (THead (Bind b)
452 u1 t3)) (THead (Flat Appl) w v) H10) in ((let H13 \def (f_equal T T (\lambda
453 (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1
454 | (TLRef _) \Rightarrow v1 | (THead _ t5 _) \Rightarrow t5])) (THead (Flat
455 Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) w v) H10) in (eq_ind T w
456 (\lambda (t5: T).((eq T (THead (Bind b) u1 t3) v) \to ((eq T (THead (Bind b)
457 u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2) \to ((not (eq B b Abst)) \to
458 ((pr0 t5 v2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat
459 Appl) w (THead (Bind Abst) u t0)))))))))) (\lambda (H14: (eq T (THead (Bind
460 b) u1 t3) v)).(eq_ind T (THead (Bind b) u1 t3) (\lambda (_: T).((eq T (THead
461 (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2) \to ((not (eq B b
462 Abst)) \to ((pr0 w v2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2
463 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))))) (\lambda (H15: (eq T
464 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t2)).(eq_ind T
465 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) (\lambda (t5:
466 T).((not (eq B b Abst)) \to ((pr0 w v2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to
467 (ty3 g c2 t5 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))) (\lambda
468 (H16: (not (eq B b Abst))).(\lambda (H17: (pr0 w v2)).(\lambda (H18: (pr0 u1
469 u2)).(\lambda (H19: (pr0 t3 t4)).(let H20 \def (eq_ind_r T v (\lambda (t5:
470 T).(\forall (c3: C).((wcpr0 c c3) \to (\forall (t6: T).((pr0 t5 t6) \to (ty3
471 g c3 t6 (THead (Bind Abst) u t0))))))) H3 (THead (Bind b) u1 t3) H14) in (let
472 H21 \def (eq_ind_r T v (\lambda (t5: T).(ty3 g c t5 (THead (Bind Abst) u
473 t0))) H2 (THead (Bind b) u1 t3) H14) in (ex_ind T (\lambda (t5: T).(ty3 g c2
474 (THead (Bind Abst) u t0) t5)) (ty3 g c2 (THead (Bind b) u2 (THead (Flat Appl)
475 (lift (S O) O v2) t4)) (THead (Flat Appl) w (THead (Bind Abst) u t0)))
476 (\lambda (x: T).(\lambda (H22: (ty3 g c2 (THead (Bind Abst) u t0) x)).(let
477 H23 \def H22 in (ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda
478 (_: T).(pc3 c2 (THead (Bind Abst) u t5) x)))) (\lambda (_: T).(\lambda (t6:
479 T).(\lambda (_: T).(ty3 g c2 u t6)))) (\lambda (t5: T).(\lambda (_:
480 T).(\lambda (_: T).(ty3 g (CHead c2 (Bind Abst) u) t0 t5)))) (\lambda (t5:
481 T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c2 (Bind Abst) u) t5 t7))))
482 (ty3 g c2 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) (THead
483 (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x0: T).(\lambda (x1:
484 T).(\lambda (x2: T).(\lambda (_: (pc3 c2 (THead (Bind Abst) u x0)
485 x)).(\lambda (H25: (ty3 g c2 u x1)).(\lambda (H26: (ty3 g (CHead c2 (Bind
486 Abst) u) t0 x0)).(\lambda (H27: (ty3 g (CHead c2 (Bind Abst) u) x0
487 x2)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3
488 c2 (THead (Bind b) u2 t5) (THead (Bind Abst) u t0))))) (\lambda (_:
489 T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c2 u2 t6)))) (\lambda (t5:
490 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind b) u2) t4 t5))))
491 (\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c2 (Bind b)
492 u2) t5 t7)))) (ty3 g c2 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
493 v2) t4)) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x3:
494 T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H28: (pc3 c2 (THead (Bind b)
495 u2 x3) (THead (Bind Abst) u t0))).(\lambda (H29: (ty3 g c2 u2 x4)).(\lambda
496 (H30: (ty3 g (CHead c2 (Bind b) u2) t4 x3)).(\lambda (_: (ty3 g (CHead c2
497 (Bind b) u2) x3 x5)).(let H32 \def (eq_ind T (lift (S O) O (THead (Bind Abst)
498 u t0)) (\lambda (t5: T).(pc3 (CHead c2 (Bind b) u2) x3 t5)) (pc3_gen_not_abst
499 b H16 c2 x3 t0 u2 u H28) (THead (Bind Abst) (lift (S O) O u) (lift (S O) (S
500 O) t0)) (lift_bind Abst u t0 (S O) O)) in (let H33 \def (eq_ind T (lift (S O)
501 O (THead (Bind Abst) u t0)) (\lambda (t5: T).(ty3 g (CHead c2 (Bind b) u2) t5
502 (lift (S O) O x))) (ty3_lift g c2 (THead (Bind Abst) u t0) x H22 (CHead c2
503 (Bind b) u2) O (S O) (drop_drop (Bind b) O c2 c2 (drop_refl c2) u2)) (THead
504 (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)) (lift_bind Abst u t0 (S
505 O) O)) in (ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
506 T).(pc3 (CHead c2 (Bind b) u2) (THead (Bind Abst) (lift (S O) O u) t5) (lift
507 (S O) O x))))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g (CHead
508 c2 (Bind b) u2) (lift (S O) O u) t6)))) (\lambda (t5: T).(\lambda (_:
509 T).(\lambda (_: T).(ty3 g (CHead (CHead c2 (Bind b) u2) (Bind Abst) (lift (S
510 O) O u)) (lift (S O) (S O) t0) t5)))) (\lambda (t5: T).(\lambda (_:
511 T).(\lambda (t7: T).(ty3 g (CHead (CHead c2 (Bind b) u2) (Bind Abst) (lift (S
512 O) O u)) t5 t7)))) (ty3 g c2 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
513 O) O v2) t4)) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x6:
514 T).(\lambda (x7: T).(\lambda (x8: T).(\lambda (_: (pc3 (CHead c2 (Bind b) u2)
515 (THead (Bind Abst) (lift (S O) O u) x6) (lift (S O) O x))).(\lambda (H35:
516 (ty3 g (CHead c2 (Bind b) u2) (lift (S O) O u) x7)).(\lambda (H36: (ty3 g
517 (CHead (CHead c2 (Bind b) u2) (Bind Abst) (lift (S O) O u)) (lift (S O) (S O)
518 t0) x6)).(\lambda (H37: (ty3 g (CHead (CHead c2 (Bind b) u2) (Bind Abst)
519 (lift (S O) O u)) x6 x8)).(ty3_conv g c2 (THead (Flat Appl) w (THead (Bind
520 Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u x0)) (ty3_appl g c2 w
521 u (H1 c2 H4 w (pr0_refl w)) (THead (Bind Abst) u t0) x0 (ty3_bind g c2 u x1
522 H25 Abst t0 x0 H26 x2 H27)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O)
523 O v2) t4)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) (THead
524 (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)))) (ty3_bind g c2 u2 x4
525 H29 b (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat Appl) (lift (S O)
526 O v2) (THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0))) (ty3_appl g
527 (CHead c2 (Bind b) u2) (lift (S O) O v2) (lift (S O) O u) (ty3_lift g c2 v2 u
528 (H1 c2 H4 v2 H17) (CHead c2 (Bind b) u2) O (S O) (drop_drop (Bind b) O c2 c2
529 (drop_refl c2) u2)) t4 (lift (S O) (S O) t0) (ty3_conv g (CHead c2 (Bind b)
530 u2) (THead (Bind Abst) (lift (S O) O u) (lift (S O) (S O) t0)) (THead (Bind
531 Abst) (lift (S O) O u) x6) (ty3_bind g (CHead c2 (Bind b) u2) (lift (S O) O
532 u) x7 H35 Abst (lift (S O) (S O) t0) x6 H36 x8 H37) t4 x3 H30 H32)) (THead
533 (Flat Appl) (lift (S O) O v2) (THead (Bind Abst) (lift (S O) O u) x6))
534 (ty3_appl g (CHead c2 (Bind b) u2) (lift (S O) O v2) (lift (S O) O u)
535 (ty3_lift g c2 v2 u (H1 c2 H4 v2 H17) (CHead c2 (Bind b) u2) O (S O)
536 (drop_drop (Bind b) O c2 c2 (drop_refl c2) u2)) (THead (Bind Abst) (lift (S
537 O) O u) (lift (S O) (S O) t0)) x6 (ty3_bind g (CHead c2 (Bind b) u2) (lift (S
538 O) O u) x7 H35 Abst (lift (S O) (S O) t0) x6 H36 x8 H37))) (eq_ind T (lift (S
539 O) O (THead (Bind Abst) u t0)) (\lambda (t5: T).(pc3 c2 (THead (Bind b) u2
540 (THead (Flat Appl) (lift (S O) O v2) t5)) (THead (Flat Appl) w (THead (Bind
541 Abst) u t0)))) (pc3_pc1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
542 v2) (lift (S O) O (THead (Bind Abst) u t0)))) (THead (Flat Appl) w (THead
543 (Bind Abst) u t0)) (pc1_pr0_u2 (THead (Flat Appl) v2 (THead (Bind b) u2 (lift
544 (S O) O (THead (Bind Abst) u t0)))) (THead (Bind b) u2 (THead (Flat Appl)
545 (lift (S O) O v2) (lift (S O) O (THead (Bind Abst) u t0)))) (pr0_upsilon b
546 H16 v2 v2 (pr0_refl v2) u2 u2 (pr0_refl u2) (lift (S O) O (THead (Bind Abst)
547 u t0)) (lift (S O) O (THead (Bind Abst) u t0)) (pr0_refl (lift (S O) O (THead
548 (Bind Abst) u t0)))) (THead (Flat Appl) w (THead (Bind Abst) u t0)) (pc1_head
549 v2 w (pc1_pr0_x v2 w H17) (THead (Bind b) u2 (lift (S O) O (THead (Bind Abst)
550 u t0))) (THead (Bind Abst) u t0) (pc1_pr0_r (THead (Bind b) u2 (lift (S O) O
551 (THead (Bind Abst) u t0))) (THead (Bind Abst) u t0) (pr0_zeta b H16 (THead
552 (Bind Abst) u t0) (THead (Bind Abst) u t0) (pr0_refl (THead (Bind Abst) u
553 t0)) u2)) (Flat Appl))) c2) (THead (Bind Abst) (lift (S O) O u) (lift (S O)
554 (S O) t0)) (lift_bind Abst u t0 (S O) O)))))))))) (ty3_gen_bind g Abst (CHead
555 c2 (Bind b) u2) (lift (S O) O u) (lift (S O) (S O) t0) (lift (S O) O x)
556 H33))))))))))) (ty3_gen_bind g b c2 u2 t4 (THead (Bind Abst) u t0) (H20 c2 H4
557 (THead (Bind b) u2 t4) (pr0_comp u1 u2 H18 t3 t4 H19 (Bind b))))))))))))
558 (ty3_gen_bind g Abst c2 u t0 x H23))))) (ty3_correct g c2 (THead (Bind b) u2
559 t4) (THead (Bind Abst) u t0) (H20 c2 H4 (THead (Bind b) u2 t4) (pr0_comp u1
560 u2 H18 t3 t4 H19 (Bind b))))))))))) t2 H15)) v H14)) v1 (sym_eq T v1 w H13)))
561 H12)) H11 H6 H7 H8 H9))) | (pr0_delta u1 u2 H6 t3 t4 H7 w0 H8) \Rightarrow
562 (\lambda (H9: (eq T (THead (Bind Abbr) u1 t3) (THead (Flat Appl) w
563 v))).(\lambda (H10: (eq T (THead (Bind Abbr) u2 w0) t2)).((let H11 \def
564 (eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (e: T).(match e in T return
565 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
566 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
567 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
568 False])])) I (THead (Flat Appl) w v) H9) in (False_ind ((eq T (THead (Bind
569 Abbr) u2 w0) t2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to ((subst0 O u2 t4 w0)
570 \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))) H11))
571 H10 H6 H7 H8))) | (pr0_zeta b H6 t3 t4 H7 u0) \Rightarrow (\lambda (H8: (eq T
572 (THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Appl) w v))).(\lambda (H9:
573 (eq T t4 t2)).((let H10 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O t3))
574 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
575 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
576 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True |
577 (Flat _) \Rightarrow False])])) I (THead (Flat Appl) w v) H8) in (False_ind
578 ((eq T t4 t2) \to ((not (eq B b Abst)) \to ((pr0 t3 t4) \to (ty3 g c2 t2
579 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) |
580 (pr0_epsilon t3 t4 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast)
581 u0 t3) (THead (Flat Appl) w v))).(\lambda (H8: (eq T t4 t2)).((let H9 \def
582 (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (e: T).(match e in T return
583 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
584 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
585 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
586 in F return (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast
587 \Rightarrow True])])])) I (THead (Flat Appl) w v) H7) in (False_ind ((eq T t4
588 t2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst)
589 u t0))))) H9)) H8 H6)))]) in (H6 (refl_equal T (THead (Flat Appl) w v))
590 (refl_equal T t2)))))))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda
591 (t3: T).(\lambda (_: (ty3 g c t2 t3)).(\lambda (H1: ((\forall (c2: C).((wcpr0
592 c c2) \to (\forall (t4: T).((pr0 t2 t4) \to (ty3 g c2 t4 t3))))))).(\lambda
593 (t0: T).(\lambda (_: (ty3 g c t3 t0)).(\lambda (H3: ((\forall (c2: C).((wcpr0
594 c c2) \to (\forall (t4: T).((pr0 t3 t4) \to (ty3 g c2 t4 t0))))))).(\lambda
595 (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t4: T).(\lambda (H5: (pr0
596 (THead (Flat Cast) t3 t2) t4)).(let H6 \def (match H5 in pr0 return (\lambda
597 (t5: T).(\lambda (t6: T).(\lambda (_: (pr0 t5 t6)).((eq T t5 (THead (Flat
598 Cast) t3 t2)) \to ((eq T t6 t4) \to (ty3 g c2 t4 (THead (Flat Cast) t0
599 t3))))))) with [(pr0_refl t5) \Rightarrow (\lambda (H6: (eq T t5 (THead (Flat
600 Cast) t3 t2))).(\lambda (H7: (eq T t5 t4)).(eq_ind T (THead (Flat Cast) t3
601 t2) (\lambda (t6: T).((eq T t6 t4) \to (ty3 g c2 t4 (THead (Flat Cast) t0
602 t3)))) (\lambda (H8: (eq T (THead (Flat Cast) t3 t2) t4)).(eq_ind T (THead
603 (Flat Cast) t3 t2) (\lambda (t6: T).(ty3 g c2 t6 (THead (Flat Cast) t0 t3)))
604 (ty3_cast g c2 t2 t3 (H1 c2 H4 t2 (pr0_refl t2)) t0 (H3 c2 H4 t3 (pr0_refl
605 t3))) t4 H8)) t5 (sym_eq T t5 (THead (Flat Cast) t3 t2) H6) H7))) | (pr0_comp
606 u1 u2 H6 t5 t6 H7 k) \Rightarrow (\lambda (H8: (eq T (THead k u1 t5) (THead
607 (Flat Cast) t3 t2))).(\lambda (H9: (eq T (THead k u2 t6) t4)).((let H10 \def
608 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
609 [(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7)
610 \Rightarrow t7])) (THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H11
611 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
612 with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t7 _)
613 \Rightarrow t7])) (THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H12
614 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
615 with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
616 \Rightarrow k0])) (THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in (eq_ind K
617 (Flat Cast) (\lambda (k0: K).((eq T u1 t3) \to ((eq T t5 t2) \to ((eq T
618 (THead k0 u2 t6) t4) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4
619 (THead (Flat Cast) t0 t3)))))))) (\lambda (H13: (eq T u1 t3)).(eq_ind T t3
620 (\lambda (t7: T).((eq T t5 t2) \to ((eq T (THead (Flat Cast) u2 t6) t4) \to
621 ((pr0 t7 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0
622 t3))))))) (\lambda (H14: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T
623 (THead (Flat Cast) u2 t6) t4) \to ((pr0 t3 u2) \to ((pr0 t7 t6) \to (ty3 g c2
624 t4 (THead (Flat Cast) t0 t3)))))) (\lambda (H15: (eq T (THead (Flat Cast) u2
625 t6) t4)).(eq_ind T (THead (Flat Cast) u2 t6) (\lambda (t7: T).((pr0 t3 u2)
626 \to ((pr0 t2 t6) \to (ty3 g c2 t7 (THead (Flat Cast) t0 t3))))) (\lambda
627 (H16: (pr0 t3 u2)).(\lambda (H17: (pr0 t2 t6)).(ex_ind T (\lambda (t7:
628 T).(ty3 g c2 t0 t7)) (ty3 g c2 (THead (Flat Cast) u2 t6) (THead (Flat Cast)
629 t0 t3)) (\lambda (x: T).(\lambda (H18: (ty3 g c2 t0 x)).(ty3_conv g c2 (THead
630 (Flat Cast) t0 t3) (THead (Flat Cast) x t0) (ty3_cast g c2 t3 t0 (H3 c2 H4 t3
631 (pr0_refl t3)) x H18) (THead (Flat Cast) u2 t6) (THead (Flat Cast) t0 u2)
632 (ty3_cast g c2 t6 u2 (ty3_conv g c2 u2 t0 (H3 c2 H4 u2 H16) t6 t3 (H1 c2 H4
633 t6 H17) (pc3_pr2_r c2 t3 u2 (pr2_free c2 t3 u2 H16))) t0 (H3 c2 H4 u2 H16))
634 (pc3_s c2 (THead (Flat Cast) t0 u2) (THead (Flat Cast) t0 t3) (pc3_pr2_r c2
635 (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 u2) (pr2_thin_dx c2 t3 u2
636 (pr2_free c2 t3 u2 H16) t0 Cast)))))) (ty3_correct g c2 t3 t0 (H3 c2 H4 t3
637 (pr0_refl t3)))))) t4 H15)) t5 (sym_eq T t5 t2 H14))) u1 (sym_eq T u1 t3
638 H13))) k (sym_eq K k (Flat Cast) H12))) H11)) H10)) H9 H6 H7))) | (pr0_beta u
639 v1 v2 H6 t5 t6 H7) \Rightarrow (\lambda (H8: (eq T (THead (Flat Appl) v1
640 (THead (Bind Abst) u t5)) (THead (Flat Cast) t3 t2))).(\lambda (H9: (eq T
641 (THead (Bind Abbr) v2 t6) t4)).((let H10 \def (eq_ind T (THead (Flat Appl) v1
642 (THead (Bind Abst) u t5)) (\lambda (e: T).(match e in T return (\lambda (_:
643 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
644 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
645 [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f in F return
646 (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast \Rightarrow
647 False])])])) I (THead (Flat Cast) t3 t2) H8) in (False_ind ((eq T (THead
648 (Bind Abbr) v2 t6) t4) \to ((pr0 v1 v2) \to ((pr0 t5 t6) \to (ty3 g c2 t4
649 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7))) | (pr0_upsilon b H6 v1 v2 H7
650 u1 u2 H8 t5 t6 H9) \Rightarrow (\lambda (H10: (eq T (THead (Flat Appl) v1
651 (THead (Bind b) u1 t5)) (THead (Flat Cast) t3 t2))).(\lambda (H11: (eq T
652 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4)).((let H12
653 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 t5)) (\lambda (e:
654 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
655 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
656 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f)
657 \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl \Rightarrow
658 True | Cast \Rightarrow False])])])) I (THead (Flat Cast) t3 t2) H10) in
659 (False_ind ((eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
660 t6)) t4) \to ((not (eq B b Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2) \to ((pr0
661 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))))) H12)) H11 H6 H7 H8
662 H9))) | (pr0_delta u1 u2 H6 t5 t6 H7 w H8) \Rightarrow (\lambda (H9: (eq T
663 (THead (Bind Abbr) u1 t5) (THead (Flat Cast) t3 t2))).(\lambda (H10: (eq T
664 (THead (Bind Abbr) u2 w) t4)).((let H11 \def (eq_ind T (THead (Bind Abbr) u1
665 t5) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort
666 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
667 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
668 \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Cast) t3
669 t2) H9) in (False_ind ((eq T (THead (Bind Abbr) u2 w) t4) \to ((pr0 u1 u2)
670 \to ((pr0 t5 t6) \to ((subst0 O u2 t6 w) \to (ty3 g c2 t4 (THead (Flat Cast)
671 t0 t3)))))) H11)) H10 H6 H7 H8))) | (pr0_zeta b H6 t5 t6 H7 u) \Rightarrow
672 (\lambda (H8: (eq T (THead (Bind b) u (lift (S O) O t5)) (THead (Flat Cast)
673 t3 t2))).(\lambda (H9: (eq T t6 t4)).((let H10 \def (eq_ind T (THead (Bind b)
674 u (lift (S O) O t5)) (\lambda (e: T).(match e in T return (\lambda (_:
675 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
676 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
677 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat
678 Cast) t3 t2) H8) in (False_ind ((eq T t6 t4) \to ((not (eq B b Abst)) \to
679 ((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7)))
680 | (pr0_epsilon t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast)
681 u t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \def
682 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
683 [(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7)
684 \Rightarrow t7])) (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7) in
685 ((let H10 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
686 T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t7
687 _) \Rightarrow t7])) (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7)
688 in (eq_ind T t3 (\lambda (_: T).((eq T t5 t2) \to ((eq T t6 t4) \to ((pr0 t5
689 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3)))))) (\lambda (H11: (eq T t5
690 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T t6 t4) \to ((pr0 t7 t6) \to (ty3 g
691 c2 t4 (THead (Flat Cast) t0 t3))))) (\lambda (H12: (eq T t6 t4)).(eq_ind T t4
692 (\lambda (t7: T).((pr0 t2 t7) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))
693 (\lambda (H13: (pr0 t2 t4)).(ex_ind T (\lambda (t7: T).(ty3 g c2 t0 t7)) (ty3
694 g c2 t4 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H14: (ty3 g c2
695 t0 x)).(ty3_conv g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
696 (ty3_cast g c2 t3 t0 (H3 c2 H4 t3 (pr0_refl t3)) x H14) t4 t3 (H1 c2 H4 t4
697 H13) (pc3_pr2_x c2 t3 (THead (Flat Cast) t0 t3) (pr2_free c2 (THead (Flat
698 Cast) t0 t3) t3 (pr0_epsilon t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2
699 t3 t0 (H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T
700 t5 t2 H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T
701 (THead (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))).
703 theorem ty3_sred_pr1:
704 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall
705 (g: G).(\forall (t: T).((ty3 g c t1 t) \to (ty3 g c t2 t)))))))
707 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1
708 t2)).(pr1_ind (\lambda (t: T).(\lambda (t0: T).(\forall (g: G).(\forall (t3:
709 T).((ty3 g c t t3) \to (ty3 g c t0 t3)))))) (\lambda (t: T).(\lambda (g:
710 G).(\lambda (t0: T).(\lambda (H0: (ty3 g c t t0)).H0)))) (\lambda (t3:
711 T).(\lambda (t4: T).(\lambda (H0: (pr0 t4 t3)).(\lambda (t5: T).(\lambda (_:
712 (pr1 t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (t: T).((ty3 g c t3 t)
713 \to (ty3 g c t5 t)))))).(\lambda (g: G).(\lambda (t: T).(\lambda (H3: (ty3 g
714 c t4 t)).(H2 g t (ty3_sred_wcpr0_pr0 g c t4 t H3 c (wcpr0_refl c) t3
715 H0))))))))))) t1 t2 H)))).
717 theorem ty3_sred_pr2:
718 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
719 (g: G).(\forall (t: T).((ty3 g c t1 t) \to (ty3 g c t2 t)))))))
721 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
722 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (g:
723 G).(\forall (t3: T).((ty3 g c0 t t3) \to (ty3 g c0 t0 t3))))))) (\lambda (c0:
724 C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda (g:
725 G).(\lambda (t: T).(\lambda (H1: (ty3 g c0 t3 t)).(ty3_sred_wcpr0_pr0 g c0 t3
726 t H1 c0 (wcpr0_refl c0) t4 H0)))))))) (\lambda (c0: C).(\lambda (d:
727 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind
728 Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3
729 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g:
730 G).(\lambda (t0: T).(\lambda (H3: (ty3 g c0 t3 t0)).(ty3_subst0 g c0 t4 t0
731 (ty3_sred_wcpr0_pr0 g c0 t3 t0 H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t
732 H2)))))))))))))) c t1 t2 H)))).
734 theorem ty3_sred_pr3:
735 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall
736 (g: G).(\forall (t: T).((ty3 g c t1 t) \to (ty3 g c t2 t)))))))
738 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1
739 t2)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (g: G).(\forall
740 (t3: T).((ty3 g c t t3) \to (ty3 g c t0 t3)))))) (\lambda (t: T).(\lambda (g:
741 G).(\lambda (t0: T).(\lambda (H0: (ty3 g c t t0)).H0)))) (\lambda (t3:
742 T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
743 (_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (t: T).((ty3 g c
744 t3 t) \to (ty3 g c t5 t)))))).(\lambda (g: G).(\lambda (t: T).(\lambda (H3:
745 (ty3 g c t4 t)).(H2 g t (ty3_sred_pr2 c t4 t3 H0 g t H3))))))))))) t1 t2
projects / helm.git / blob