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