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/props".
24 \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e
25 t1 t2) \to (\forall (c: C).(\forall (d: nat).(\forall (h: nat).((drop h d c
26 e) \to (ty3 g c (lift h d t1) (lift h d t2))))))))))
28 \lambda (g: G).(\lambda (e: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
29 (H: (ty3 g e t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda (t0:
30 T).(\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
31 (ty3 g c0 (lift h d t) (lift h d t0))))))))) (\lambda (c: C).(\lambda (t0:
32 T).(\lambda (t: T).(\lambda (_: (ty3 g c t0 t)).(\lambda (H1: ((\forall (c0:
33 C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h
34 d t0) (lift h d t)))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (_: (ty3
35 g c u t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
36 nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
37 t3)))))))).(\lambda (H4: (pc3 c t3 t0)).(\lambda (c0: C).(\lambda (d:
38 nat).(\lambda (h: nat).(\lambda (H5: (drop h d c0 c)).(ty3_conv g c0 (lift h
39 d t0) (lift h d t) (H1 c0 d h H5) (lift h d u) (lift h d t3) (H3 c0 d h H5)
40 (pc3_lift c0 c h d H5 t3 t0 H4)))))))))))))))) (\lambda (c: C).(\lambda (m:
41 nat).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (_: (drop
42 h d c0 c)).(eq_ind_r T (TSort m) (\lambda (t: T).(ty3 g c0 t (lift h d (TSort
43 (next g m))))) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(ty3 g c0
44 (TSort m) t)) (ty3_sort g c0 m) (lift h d (TSort (next g m))) (lift_sort
45 (next g m) h d)) (lift h d (TSort m)) (lift_sort m h d)))))))) (\lambda (n:
46 nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
47 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
48 t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
49 nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
50 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
51 (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
52 (lift (S n) O t))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
53 n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3 (CHead d (Bind Abbr) u) H0)
54 in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0)))
55 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n) e0 e1))) (\lambda (_:
56 C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0
57 (TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x0: C).(\lambda (x1:
58 C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
59 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind
60 nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S
61 n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0
62 (S n)) H9 Abbr d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1
63 (Bind Abbr) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h (minus d0
64 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
65 (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h (minus
66 d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x d)).(eq_ind_r T
67 (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t))))
68 (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3 g c0 (TLRef
69 n) (lift h n0 (lift (S n) O t)))) (eq_ind_r T (lift (S n) O (lift h (minus d0
70 (S n)) t)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda
71 (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))))
72 (ty3_abbr g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0 (CHead x
73 (Bind Abbr) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus d0 (S n))
74 t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
75 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
76 n) O t)) (lift_d t h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
77 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
78 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
79 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat
80 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
81 t)))) (eq_ind_r T (lift (plus h (S n)) O t) (\lambda (t0: T).(ty3 g c0 (TLRef
82 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
83 (TLRef (plus n h)) (lift n0 O t))) (ty3_abbr g (plus n h) c0 d u
84 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) t H1) (plus
85 h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
86 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
87 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
88 (plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
89 d0 H4)))))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d:
90 C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda
91 (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall
92 (d0: nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u)
93 (lift h d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h:
94 nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0
95 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5
96 \def (drop_getl_trans_le n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3
97 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_:
98 C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n)
99 e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst)
100 u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda
101 (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop
102 h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let
103 H9 \def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S
104 (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0
105 h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0
106 (CHead c1 (Bind Abst) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h
107 (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S
108 n) O u))) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift
109 h (minus d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x
110 d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S
111 n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3
112 g c0 (TLRef n) (lift h n0 (lift (S n) O u)))) (eq_ind_r T (lift (S n) O (lift
113 h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat
114 d0 (\lambda (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S
115 n)) u)))) (ty3_abst g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0
116 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus
117 d0 (S n)) t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
118 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
119 n) O u)) (lift_d u h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
120 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
121 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
122 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat
123 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
124 u)))) (eq_ind_r T (lift (plus h (S n)) O u) (\lambda (t0: T).(ty3 g c0 (TLRef
125 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
126 (TLRef (plus n h)) (lift n0 O u))) (ty3_abst g (plus n h) c0 d u
127 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) t H1) (plus
128 h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
129 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
130 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
131 (plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
132 d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t:
133 T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
134 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
135 t)))))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3
136 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
137 nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
138 (lift h d t0) (lift h d t3)))))))).(\lambda (c0: C).(\lambda (d:
139 nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
140 (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t4: T).(ty3 g c0
141 t4 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
142 u) (lift h (s (Bind b) d) t3)) (\lambda (t4: T).(ty3 g c0 (THead (Bind b)
143 (lift h d u) (lift h (s (Bind b) d) t0)) t4)) (ty3_bind g c0 (lift h d u)
144 (lift h d t) (H1 c0 d h H4) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
145 c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H4 b u))) (lift h
146 d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) (lift h d (THead
147 (Bind b) u t0)) (lift_head (Bind b) u t0 h d)))))))))))))))) (\lambda (c:
148 C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1:
149 ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
150 (ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda (v: T).(\lambda (t:
151 T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u t))).(\lambda (H3: ((\forall
152 (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0
153 (lift h d v) (lift h d (THead (Bind Abst) u t))))))))).(\lambda (c0:
154 C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0
155 c)).(eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v))
156 (\lambda (t0: T).(ty3 g c0 t0 (lift h d (THead (Flat Appl) w (THead (Bind
157 Abst) u t))))) (eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat
158 Appl) d) (THead (Bind Abst) u t))) (\lambda (t0: T).(ty3 g c0 (THead (Flat
159 Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) t0)) (eq_ind_r T (THead
160 (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s (Flat
161 Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w)
162 (lift h (s (Flat Appl) d) v)) (THead (Flat Appl) (lift h d w) t0))) (ty3_appl
163 g c0 (lift h d w) (lift h d u) (H1 c0 d h H4) (lift h d v) (lift h (S d) t)
164 (eq_ind T (lift h d (THead (Bind Abst) u t)) (\lambda (t0: T).(ty3 g c0 (lift
165 h d v) t0)) (H3 c0 d h H4) (THead (Bind Abst) (lift h d u) (lift h (S d) t))
166 (lift_bind Abst u t h d))) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t))
167 (lift_head (Bind Abst) u t h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
168 w (THead (Bind Abst) u t))) (lift_head (Flat Appl) w (THead (Bind Abst) u t)
169 h d)) (lift h d (THead (Flat Appl) w v)) (lift_head (Flat Appl) w v h
170 d))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda
171 (_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
172 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t0) (lift h d
173 t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3:
174 ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
175 (ty3 g c0 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d:
176 nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
177 (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) (\lambda (t: T).(ty3
178 g c0 t (lift h d (THead (Flat Cast) t4 t3)))) (eq_ind_r T (THead (Flat Cast)
179 (lift h d t4) (lift h (s (Flat Cast) d) t3)) (\lambda (t: T).(ty3 g c0 (THead
180 (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) t)) (ty3_cast g c0
181 (lift h (s (Flat Cast) d) t0) (lift h (s (Flat Cast) d) t3) (H1 c0 (s (Flat
182 Cast) d) h H4) (lift h d t4) (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t4
183 t3)) (lift_head (Flat Cast) t4 t3 h d)) (lift h d (THead (Flat Cast) t3 t0))
184 (lift_head (Flat Cast) t3 t0 h d)))))))))))))) e t1 t2 H))))).
187 \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
188 t1 t2) \to (ex T (\lambda (t: T).(ty3 g c t2 t)))))))
190 \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
191 (H: (ty3 g c t1 t2)).(ty3_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda
192 (t0: T).(ex T (\lambda (t3: T).(ty3 g c0 t0 t3)))))) (\lambda (c0:
193 C).(\lambda (t0: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 t0 t)).(\lambda
194 (_: (ex T (\lambda (t3: T).(ty3 g c0 t t3)))).(\lambda (u: T).(\lambda (t3:
195 T).(\lambda (_: (ty3 g c0 u t3)).(\lambda (_: (ex T (\lambda (t4: T).(ty3 g
196 c0 t3 t4)))).(\lambda (_: (pc3 c0 t3 t0)).(ex_intro T (\lambda (t4: T).(ty3 g
197 c0 t0 t4)) t H0))))))))))) (\lambda (c0: C).(\lambda (m: nat).(ex_intro T
198 (\lambda (t: T).(ty3 g c0 (TSort (next g m)) t)) (TSort (next g (next g m)))
199 (ty3_sort g c0 (next g m))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
200 C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr)
201 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (H2: (ex T (\lambda
202 (t0: T).(ty3 g d t t0)))).(let H3 \def H2 in (ex_ind T (\lambda (t0: T).(ty3
203 g d t t0)) (ex T (\lambda (t0: T).(ty3 g c0 (lift (S n) O t) t0))) (\lambda
204 (x: T).(\lambda (H4: (ty3 g d t x)).(ex_intro T (\lambda (t0: T).(ty3 g c0
205 (lift (S n) O t) t0)) (lift (S n) O x) (ty3_lift g d t x H4 c0 O (S n)
206 (getl_drop Abbr c0 d u n H0))))) H3)))))))))) (\lambda (n: nat).(\lambda (c0:
207 C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind
208 Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (_: (ex T
209 (\lambda (t0: T).(ty3 g d t t0)))).(ex_intro T (\lambda (t0: T).(ty3 g c0
210 (lift (S n) O u) t0)) (lift (S n) O t) (ty3_lift g d u t H1 c0 O (S n)
211 (getl_drop Abst c0 d u n H0))))))))))) (\lambda (c0: C).(\lambda (u:
212 T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: (ex T (\lambda
213 (t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3:
214 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (H3: (ex T
215 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(let H4 \def H3 in
216 (ex_ind T (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)) (ex T
217 (\lambda (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4))) (\lambda (x:
218 T).(\lambda (H5: (ty3 g (CHead c0 (Bind b) u) t3 x)).(ex_intro T (\lambda
219 (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4)) (THead (Bind b) u x) (ty3_bind g
220 c0 u t H0 b t3 x H5)))) H4)))))))))))) (\lambda (c0: C).(\lambda (w:
221 T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T (\lambda
222 (t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g
223 c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: T).(ty3 g c0
224 (THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T (\lambda (t0:
225 T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w
226 (THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_: (ty3 g c0 u
227 x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0 (THead (Bind
228 Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead
229 (Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g c0 (THead (Bind
230 Abst) u t) x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0
231 (THead (Bind Abst) u t3) x0))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u
232 t0))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t
233 t3))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind
234 Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0
235 (THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3 g c0 u x2)).(\lambda (H10:
236 (ty3 g (CHead c0 (Bind Abst) u) t x1)).(ex_intro T (\lambda (t0: T).(ty3 g c0
237 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat Appl) w
238 (THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u t) x1
239 (ty3_bind g c0 u x2 H9 Abst t x1 H10)))))))) (ty3_gen_bind g Abst c0 u t x0
240 H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3:
241 T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g
242 c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 t3 t4)).(\lambda (H3:
243 (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def H3 in (ex_ind T
244 (\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g c0 (THead (Flat
245 Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T
246 (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x
247 t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
250 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
251 t1) \to (\forall (t2: T).((ty3 g c u t2) \to (pc3 c t1 t2)))))))
253 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H:
254 (ty3 g c u t1)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
255 T).(\forall (t2: T).((ty3 g c0 t t2) \to (pc3 c0 t0 t2)))))) (\lambda (c0:
256 C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda
257 (_: ((\forall (t3: T).((ty3 g c0 t2 t3) \to (pc3 c0 t t3))))).(\lambda (u0:
258 T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H3: ((\forall
259 (t3: T).((ty3 g c0 u0 t3) \to (pc3 c0 t0 t3))))).(\lambda (H4: (pc3 c0 t0
260 t2)).(\lambda (t3: T).(\lambda (H5: (ty3 g c0 u0 t3)).(pc3_t t0 c0 t2 (pc3_s
261 c0 t2 t0 H4) t3 (H3 t3 H5)))))))))))))) (\lambda (c0: C).(\lambda (m:
262 nat).(\lambda (t2: T).(\lambda (H0: (ty3 g c0 (TSort m) t2)).(ty3_gen_sort g
263 c0 t2 m H0))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda
264 (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr) u0))).(\lambda (t:
265 T).(\lambda (_: (ty3 g d u0 t)).(\lambda (H2: ((\forall (t2: T).((ty3 g d u0
266 t2) \to (pc3 d t t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n)
267 t2)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
268 T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
269 (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1:
270 T).(\lambda (t0: T).(ty3 g e u1 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
271 (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e:
272 C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u1)))))
273 (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))) (pc3 c0
274 (lift (S n) O t) t2) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_:
275 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
276 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
277 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T
278 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
279 t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e
280 (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g
281 e u1 t0)))) (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1:
282 T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x2) t2)).(\lambda
283 (H6: (getl n c0 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g x0 x1
284 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n
285 c0 c1)) H0 (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n
286 H0 (CHead x0 (Bind Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e:
287 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
288 (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind
289 Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr)
290 x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return
291 (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t0)
292 \Rightarrow t0])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
293 (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
294 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
295 T).(getl n c0 (CHead x0 (Bind Abbr) t0))) H8 u0 H10) in (let H13 \def
296 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
297 (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind Abbr) u0))) H12 d
298 H11) in (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3 g c1 u0 x2)) H13 d
299 H11) in (pc3_t (lift (S n) O x2) c0 (lift (S n) O t) (pc3_lift c0 d (S n) O
300 (getl_drop Abbr c0 d u0 n H14) t x2 (H2 x2 H15)) t2 H5))))))) H9)))))))))
301 H4)) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
302 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
303 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
304 T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_:
305 C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda
306 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst)
307 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))
308 (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
309 T).(\lambda (_: (pc3 c0 (lift (S n) O x1) t2)).(\lambda (H6: (getl n c0
310 (CHead x0 (Bind Abst) x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def
311 (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead
312 x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0
313 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abbr) u0)
314 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
315 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
316 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
317 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
318 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abst)
319 x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abst) x1)
320 H6)) in (False_ind (pc3 c0 (lift (S n) O t) t2) H9))))))))) H4))
321 (ty3_gen_lref g c0 t2 n H3)))))))))))) (\lambda (n: nat).(\lambda (c0:
322 C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind
323 Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_:
324 ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t t2))))).(\lambda (t2:
325 T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(or_ind (ex3_3 C T T (\lambda (_:
326 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
327 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
328 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))
329 (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift
330 (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
331 c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
332 (t0: T).(ty3 g e u1 t0))))) (pc3 c0 (lift (S n) O u0) t2) (\lambda (H4:
333 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift
334 (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
335 c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
336 (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
337 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
338 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
339 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O
340 u0) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3
341 c0 (lift (S n) O x2) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abbr)
342 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind
343 Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abbr) x1)
344 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
345 (let H9 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (ee: C).(match ee in
346 C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k
347 _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
348 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
349 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
350 \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d
351 (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in (False_ind (pc3 c0
352 (lift (S n) O u0) t2) H9))))))))) H4)) (\lambda (H4: (ex3_3 C T T (\lambda
353 (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2))))
354 (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
355 Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1
356 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
357 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
358 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
359 T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O u0) t2) (\lambda
360 (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O
361 x1) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abst) x1))).(\lambda (H7:
362 (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda
363 (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d
364 (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (f_equal
365 C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
366 \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u0)
367 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead
368 x0 (Bind Abst) x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match
369 e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _
370 t0) \Rightarrow t0])) (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
371 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in
372 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
373 T).(getl n c0 (CHead x0 (Bind Abst) t0))) H8 u0 H10) in (let H13 \def
374 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
375 (eq_ind_r T x1 (\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)) H5 u0 H10) in
376 (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind
377 Abst) u0))) H12 d H11) in (let H16 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3
378 g c1 u0 x2)) H13 d H11) in H14))))))) H9))))))))) H4)) (ty3_gen_lref g c0 t2
379 n H3)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t: T).(\lambda
380 (_: (ty3 g c0 u0 t)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 u0 t2) \to
381 (pc3 c0 t t2))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t2: T).(\lambda
382 (_: (ty3 g (CHead c0 (Bind b) u0) t0 t2)).(\lambda (H3: ((\forall (t3:
383 T).((ty3 g (CHead c0 (Bind b) u0) t0 t3) \to (pc3 (CHead c0 (Bind b) u0) t2
384 t3))))).(\lambda (t3: T).(\lambda (H4: (ty3 g c0 (THead (Bind b) u0 t0)
385 t3)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
386 u0 t4) t3))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda
387 (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u0) t0 t4))) (pc3 c0 (THead
388 (Bind b) u0 t2) t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0
389 (THead (Bind b) u0 x0) t3)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H7: (ty3
390 g (CHead c0 (Bind b) u0) t0 x0)).(pc3_t (THead (Bind b) u0 x0) c0 (THead
391 (Bind b) u0 t2) (pc3_head_2 c0 u0 t2 x0 (Bind b) (H3 x0 H7)) t3 H5))))))
392 (ty3_gen_bind g b c0 u0 t0 t3 H4)))))))))))))) (\lambda (c0: C).(\lambda (w:
393 T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2:
394 T).((ty3 g c0 w t2) \to (pc3 c0 u0 t2))))).(\lambda (v: T).(\lambda (t:
395 T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3:
396 ((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0 (THead (Bind Abst) u0 t)
397 t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0 (THead (Flat Appl) w v)
398 t2)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
399 Appl) w (THead (Bind Abst) u1 t0)) t2))) (\lambda (u1: T).(\lambda (t0:
400 T).(ty3 g c0 v (THead (Bind Abst) u1 t0)))) (\lambda (u1: T).(\lambda (_:
401 T).(ty3 g c0 w u1))) (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t))
402 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0 (THead (Flat
403 Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g c0 v (THead
404 (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(pc3_t (THead (Flat Appl)
405 w (THead (Bind Abst) x0 x1)) c0 (THead (Flat Appl) w (THead (Bind Abst) u0
406 t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0 x1) (H3
407 (THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0 w v t2
408 H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: T).(\lambda
409 (_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 t0 t3) \to
410 (pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2 t3)).(\lambda
411 (H3: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 t4))))).(\lambda (t4:
412 T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0) t4)).(ex3_ind T (\lambda
413 (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t0
414 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) (pc3 c0 (THead (Flat Cast) t3 t2) t4)
415 (\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead (Flat Cast) x0 t2)
416 t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g c0 t2 x0)).(pc3_t
417 (THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) (pc3_head_1 c0 t3 x0
418 (H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 t0 t2 t4
419 H4)))))))))))) c u t1 H))))).
421 theorem ty3_gen_abst_abst:
422 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall
423 (t2: T).((ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (ex2
424 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst)
427 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda
428 (t2: T).(\lambda (H: (ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u
429 t2))).(ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) u t2) t)) (ex2 T
430 (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u)
431 t1 t2))) (\lambda (x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2)
432 x)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c (THead (Bind Abst)
433 u t3) x))) (\lambda (_: T).(\lambda (t: T).(ty3 g c u t))) (\lambda (t3:
434 T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t2 t3))) (ex2 T (\lambda
435 (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)))
436 (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c (THead (Bind Abst) u
437 x0) x)).(\lambda (_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c (Bind
438 Abst) u) t2 x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c
439 (THead (Bind Abst) u t3) (THead (Bind Abst) u t2)))) (\lambda (_: T).(\lambda
440 (t: T).(ty3 g c u t))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c (Bind
441 Abst) u) t1 t3))) (ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3
442 g (CHead c (Bind Abst) u) t1 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
443 (H4: (pc3 c (THead (Bind Abst) u x2) (THead (Bind Abst) u t2))).(\lambda (H5:
444 (ty3 g c u x3)).(\lambda (H6: (ty3 g (CHead c (Bind Abst) u) t1 x2)).(let H_y
445 \def (pc3_gen_abst_shift c u x2 t2 H4) in (ex_intro2 T (\lambda (w: T).(ty3 g
446 c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x3 H5
447 (ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x2 H6 H_y))))))))
448 (ty3_gen_bind g Abst c u t1 (THead (Bind Abst) u t2) H))))))) (ty3_gen_bind g
449 Abst c u t2 x H0)))) (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind
450 Abst) u t2) H))))))).
452 theorem ty3_typecheck:
453 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t
454 v) \to (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)))))))
456 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (v: T).(\lambda (H:
457 (ty3 g c t v)).(ex_ind T (\lambda (t0: T).(ty3 g c v t0)) (ex T (\lambda (u:
458 T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g
459 c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u))
460 (THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v
projects / helm.git / blob