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/csubt/drop".
19 include "csubt/defs.ma".
21 include "drop/fwd.ma".
23 theorem csubt_drop_flat:
24 \forall (g: G).(\forall (f: F).(\forall (n: nat).(\forall (c1: C).(\forall
25 (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1
26 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
27 (d2: C).(drop n O c2 (CHead d2 (Flat f) u))))))))))))
29 \lambda (g: G).(\lambda (f: F).(\lambda (n: nat).(nat_ind (\lambda (n0:
30 nat).(\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
31 C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda
32 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Flat f)
33 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
34 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
35 (Flat f) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
36 (CHead d1 (Flat f) u) (drop_gen_refl c1 (CHead d1 (Flat f) u) H0)) in (let H2
37 \def (match H1 in csubt return (\lambda (c: C).(\lambda (c0: C).(\lambda (_:
38 (csubt ? c c0)).((eq C c (CHead d1 (Flat f) u)) \to ((eq C c0 c2) \to (ex2 C
39 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2
40 (Flat f) u))))))))) with [(csubt_sort n0) \Rightarrow (\lambda (H2: (eq C
41 (CSort n0) (CHead d1 (Flat f) u))).(\lambda (H3: (eq C (CSort n0) c2)).((let
42 H4 \def (eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda
43 (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
44 False])) I (CHead d1 (Flat f) u) H2) in (False_ind ((eq C (CSort n0) c2) \to
45 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead
46 d2 (Flat f) u))))) H4)) H3))) | (csubt_head c0 c3 H2 k u0) \Rightarrow
47 (\lambda (H3: (eq C (CHead c0 k u0) (CHead d1 (Flat f) u))).(\lambda (H4: (eq
48 C (CHead c3 k u0) c2)).((let H5 \def (f_equal C T (\lambda (e: C).(match e in
49 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
50 \Rightarrow t])) (CHead c0 k u0) (CHead d1 (Flat f) u) H3) in ((let H6 \def
51 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
52 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k u0)
53 (CHead d1 (Flat f) u) H3) in ((let H7 \def (f_equal C C (\lambda (e:
54 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
55 (CHead c _ _) \Rightarrow c])) (CHead c0 k u0) (CHead d1 (Flat f) u) H3) in
56 (eq_ind C d1 (\lambda (c: C).((eq K k (Flat f)) \to ((eq T u0 u) \to ((eq C
57 (CHead c3 k u0) c2) \to ((csubt g c c3) \to (ex2 C (\lambda (d2: C).(csubt g
58 d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Flat f) u))))))))) (\lambda
59 (H8: (eq K k (Flat f))).(eq_ind K (Flat f) (\lambda (k0: K).((eq T u0 u) \to
60 ((eq C (CHead c3 k0 u0) c2) \to ((csubt g d1 c3) \to (ex2 C (\lambda (d2:
61 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Flat f)
62 u)))))))) (\lambda (H9: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((eq C
63 (CHead c3 (Flat f) t) c2) \to ((csubt g d1 c3) \to (ex2 C (\lambda (d2:
64 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Flat f) u)))))))
65 (\lambda (H10: (eq C (CHead c3 (Flat f) u) c2)).(eq_ind C (CHead c3 (Flat f)
66 u) (\lambda (c: C).((csubt g d1 c3) \to (ex2 C (\lambda (d2: C).(csubt g d1
67 d2)) (\lambda (d2: C).(drop O O c (CHead d2 (Flat f) u)))))) (\lambda (H11:
68 (csubt g d1 c3)).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
69 C).(drop O O (CHead c3 (Flat f) u) (CHead d2 (Flat f) u))) c3 H11 (drop_refl
70 (CHead c3 (Flat f) u)))) c2 H10)) u0 (sym_eq T u0 u H9))) k (sym_eq K k (Flat
71 f) H8))) c0 (sym_eq C c0 d1 H7))) H6)) H5)) H4 H2))) | (csubt_void c0 c3 H2 b
72 H3 u1 u2) \Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind Void) u1) (CHead d1
73 (Flat f) u))).(\lambda (H5: (eq C (CHead c3 (Bind b) u2) c2)).((let H6 \def
74 (eq_ind C (CHead c0 (Bind Void) u1) (\lambda (e: C).(match e in C return
75 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
76 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
77 \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1 (Flat f) u)
78 H4) in (False_ind ((eq C (CHead c3 (Bind b) u2) c2) \to ((csubt g c0 c3) \to
79 ((not (eq B b Void)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
80 (d2: C).(drop O O c2 (CHead d2 (Flat f) u))))))) H6)) H5 H2 H3))) |
81 (csubt_abst c0 c3 H2 u0 t H3) \Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind
82 Abst) t) (CHead d1 (Flat f) u))).(\lambda (H5: (eq C (CHead c3 (Bind Abbr)
83 u0) c2)).((let H6 \def (eq_ind C (CHead c0 (Bind Abst) t) (\lambda (e:
84 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
85 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
86 with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1
87 (Flat f) u) H4) in (False_ind ((eq C (CHead c3 (Bind Abbr) u0) c2) \to
88 ((csubt g c0 c3) \to ((ty3 g c3 u0 t) \to (ex2 C (\lambda (d2: C).(csubt g d1
89 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Flat f) u))))))) H6)) H5 H2
90 H3)))]) in (H2 (refl_equal C (CHead d1 (Flat f) u)) (refl_equal C
91 c2)))))))))) (\lambda (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2:
92 C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1
93 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
94 (d2: C).(drop n0 O c2 (CHead d2 (Flat f) u)))))))))))).(\lambda (c1:
95 C).(\lambda (c2: C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c:
96 C).(\lambda (c0: C).(\forall (d1: C).(\forall (u: T).((drop (S n0) O c (CHead
97 d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
98 C).(drop (S n0) O c0 (CHead d2 (Flat f) u))))))))) (\lambda (n1:
99 nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n0) O (CSort n1)
100 (CHead d1 (Flat f) u))).(let H2 \def (match H1 in drop return (\lambda (n2:
101 nat).(\lambda (n3: nat).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop
102 n2 n3 c c0)).((eq nat n2 (S n0)) \to ((eq nat n3 O) \to ((eq C c (CSort n1))
103 \to ((eq C c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1
104 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Flat f)
105 u))))))))))))) with [(drop_refl c) \Rightarrow (\lambda (H2: (eq nat O (S
106 n0))).(\lambda (H3: (eq nat O O)).(\lambda (H4: (eq C c (CSort n1))).(\lambda
107 (H5: (eq C c (CHead d1 (Flat f) u))).((let H6 \def (eq_ind nat O (\lambda (e:
108 nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
109 | (S _) \Rightarrow False])) I (S n0) H2) in (False_ind ((eq nat O O) \to
110 ((eq C c (CSort n1)) \to ((eq C c (CHead d1 (Flat f) u)) \to (ex2 C (\lambda
111 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
112 (Flat f) u))))))) H6)) H3 H4 H5))))) | (drop_drop k h c e H2 u0) \Rightarrow
113 (\lambda (H3: (eq nat (S h) (S n0))).(\lambda (H4: (eq nat O O)).(\lambda
114 (H5: (eq C (CHead c k u0) (CSort n1))).(\lambda (H6: (eq C e (CHead d1 (Flat
115 f) u))).((let H7 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat
116 return (\lambda (_: nat).nat) with [O \Rightarrow h | (S n2) \Rightarrow
117 n2])) (S h) (S n0) H3) in (eq_ind nat n0 (\lambda (n2: nat).((eq nat O O) \to
118 ((eq C (CHead c k u0) (CSort n1)) \to ((eq C e (CHead d1 (Flat f) u)) \to
119 ((drop (r k n2) O c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
120 (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Flat f) u))))))))) (\lambda (_:
121 (eq nat O O)).(\lambda (H9: (eq C (CHead c k u0) (CSort n1))).(let H10 \def
122 (eq_ind C (CHead c k u0) (\lambda (e0: C).(match e0 in C return (\lambda (_:
123 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow
124 True])) I (CSort n1) H9) in (False_ind ((eq C e (CHead d1 (Flat f) u)) \to
125 ((drop (r k n0) O c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
126 (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)))))) H10)))) h
127 (sym_eq nat h n0 H7))) H4 H5 H6 H2))))) | (drop_skip k h d c e H2 u0)
128 \Rightarrow (\lambda (H3: (eq nat h (S n0))).(\lambda (H4: (eq nat (S d)
129 O)).(\lambda (H5: (eq C (CHead c k (lift h (r k d) u0)) (CSort n1))).(\lambda
130 (H6: (eq C (CHead e k u0) (CHead d1 (Flat f) u))).(eq_ind nat (S n0) (\lambda
131 (n2: nat).((eq nat (S d) O) \to ((eq C (CHead c k (lift n2 (r k d) u0))
132 (CSort n1)) \to ((eq C (CHead e k u0) (CHead d1 (Flat f) u)) \to ((drop n2 (r
133 k d) c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
134 (S n0) O (CSort n1) (CHead d2 (Flat f) u))))))))) (\lambda (H7: (eq nat (S d)
135 O)).(let H8 \def (eq_ind nat (S d) (\lambda (e0: nat).(match e0 in nat return
136 (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]))
137 I O H7) in (False_ind ((eq C (CHead c k (lift (S n0) (r k d) u0)) (CSort n1))
138 \to ((eq C (CHead e k u0) (CHead d1 (Flat f) u)) \to ((drop (S n0) (r k d) c
139 e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0)
140 O (CSort n1) (CHead d2 (Flat f) u))))))) H8))) h (sym_eq nat h (S n0) H3) H4
141 H5 H6 H2)))))]) in (H2 (refl_equal nat (S n0)) (refl_equal nat O) (refl_equal
142 C (CSort n1)) (refl_equal C (CHead d1 (Flat f) u)))))))) (\lambda (c0:
143 C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (H2: ((\forall
144 (d1: C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C
145 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead
146 d2 (Flat f) u))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u:
147 T).(\forall (d1: C).(\forall (u0: T).((drop (S n0) O (CHead c0 k0 u) (CHead
148 d1 (Flat f) u0)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
149 C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Flat f) u0))))))))) (\lambda (b:
150 B).(\lambda (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H3: (drop (S
151 n0) O (CHead c0 (Bind b) u) (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2:
152 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0)))
153 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
154 (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4:
155 (csubt g d1 x)).(\lambda (H5: (drop n0 O c3 (CHead x (Flat f)
156 u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
157 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Bind
158 b) n0 c3 (CHead x (Flat f) u0) H5 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop
159 (Bind b) c0 (CHead d1 (Flat f) u0) u n0 H3)))))))) (\lambda (f0: F).(\lambda
160 (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead
161 c0 (Flat f0) u) (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g
162 d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f) u0))) (ex2 C
163 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
164 (Flat f0) u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g
165 d1 x)).(\lambda (H5: (drop (S n0) O c3 (CHead x (Flat f) u0))).(ex_intro2 C
166 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
167 (Flat f0) u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Flat f0) n0 c3 (CHead
168 x (Flat f) u0) H5 u))))) (H2 d1 u0 (drop_gen_drop (Flat f0) c0 (CHead d1
169 (Flat f) u0) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
170 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
171 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
172 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
173 u))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
174 T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S
175 n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u))).(ex2_ind C (\lambda
176 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f)
177 u))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
178 (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)))) (\lambda (x: C).(\lambda (H5:
179 (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Flat f) u))).(ex_intro2
180 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
181 (Bind b) u2) (CHead d2 (Flat f) u))) x H5 (drop_drop (Bind b) n0 c3 (CHead x
182 (Flat f) u) H6 u2))))) (H c0 c3 H1 d1 u (drop_gen_drop (Bind Void) c0 (CHead
183 d1 (Flat f) u) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3:
184 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
185 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
186 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
187 u))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c3 u
188 t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H4: (drop (S n0) O (CHead c0
189 (Bind Abst) t) (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g
190 d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0))) (ex2 C
191 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
192 (Bind Abbr) u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H5: (csubt
193 g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Flat f) u0))).(ex_intro2 C
194 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
195 (Bind Abbr) u) (CHead d2 (Flat f) u0))) x H5 (drop_drop (Bind Abbr) n0 c3
196 (CHead x (Flat f) u0) H6 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind Abst)
197 c0 (CHead d1 (Flat f) u0) t n0 H4))))))))))))) c1 c2 H0)))))) n))).
199 theorem csubt_drop_abbr:
200 \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
201 c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind
202 Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
203 n O c2 (CHead d2 (Bind Abbr) u)))))))))))
205 \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
206 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u:
207 T).((drop n0 O c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
208 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr)
209 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
210 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
211 (Bind Abbr) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
212 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H0)) in
213 (let H2 \def (match H1 in csubt return (\lambda (c: C).(\lambda (c0:
214 C).(\lambda (_: (csubt ? c c0)).((eq C c (CHead d1 (Bind Abbr) u)) \to ((eq C
215 c0 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O
216 O c2 (CHead d2 (Bind Abbr) u))))))))) with [(csubt_sort n0) \Rightarrow
217 (\lambda (H2: (eq C (CSort n0) (CHead d1 (Bind Abbr) u))).(\lambda (H3: (eq C
218 (CSort n0) c2)).((let H4 \def (eq_ind C (CSort n0) (\lambda (e: C).(match e
219 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _
220 _ _) \Rightarrow False])) I (CHead d1 (Bind Abbr) u) H2) in (False_ind ((eq C
221 (CSort n0) c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
222 C).(drop O O c2 (CHead d2 (Bind Abbr) u))))) H4)) H3))) | (csubt_head c0 c3
223 H2 k u0) \Rightarrow (\lambda (H3: (eq C (CHead c0 k u0) (CHead d1 (Bind
224 Abbr) u))).(\lambda (H4: (eq C (CHead c3 k u0) c2)).((let H5 \def (f_equal C
225 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
226 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k u0) (CHead d1
227 (Bind Abbr) u) H3) in ((let H6 \def (f_equal C K (\lambda (e: C).(match e in
228 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
229 \Rightarrow k0])) (CHead c0 k u0) (CHead d1 (Bind Abbr) u) H3) in ((let H7
230 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
231 with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k
232 u0) (CHead d1 (Bind Abbr) u) H3) in (eq_ind C d1 (\lambda (c: C).((eq K k
233 (Bind Abbr)) \to ((eq T u0 u) \to ((eq C (CHead c3 k u0) c2) \to ((csubt g c
234 c3) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O
235 c2 (CHead d2 (Bind Abbr) u))))))))) (\lambda (H8: (eq K k (Bind
236 Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T u0 u) \to ((eq C (CHead
237 c3 k0 u0) c2) \to ((csubt g d1 c3) \to (ex2 C (\lambda (d2: C).(csubt g d1
238 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u)))))))) (\lambda
239 (H9: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c3 (Bind Abbr) t)
240 c2) \to ((csubt g d1 c3) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
241 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u))))))) (\lambda (H10:
242 (eq C (CHead c3 (Bind Abbr) u) c2)).(eq_ind C (CHead c3 (Bind Abbr) u)
243 (\lambda (c: C).((csubt g d1 c3) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
244 (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abbr) u)))))) (\lambda (H11:
245 (csubt g d1 c3)).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
246 C).(drop O O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u))) c3 H11
247 (drop_refl (CHead c3 (Bind Abbr) u)))) c2 H10)) u0 (sym_eq T u0 u H9))) k
248 (sym_eq K k (Bind Abbr) H8))) c0 (sym_eq C c0 d1 H7))) H6)) H5)) H4 H2))) |
249 (csubt_void c0 c3 H2 b H3 u1 u2) \Rightarrow (\lambda (H4: (eq C (CHead c0
250 (Bind Void) u1) (CHead d1 (Bind Abbr) u))).(\lambda (H5: (eq C (CHead c3
251 (Bind b) u2) c2)).((let H6 \def (eq_ind C (CHead c0 (Bind Void) u1) (\lambda
252 (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
253 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
254 with [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with
255 [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True]) |
256 (Flat _) \Rightarrow False])])) I (CHead d1 (Bind Abbr) u) H4) in (False_ind
257 ((eq C (CHead c3 (Bind b) u2) c2) \to ((csubt g c0 c3) \to ((not (eq B b
258 Void)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O
259 O c2 (CHead d2 (Bind Abbr) u))))))) H6)) H5 H2 H3))) | (csubt_abst c0 c3 H2
260 u0 t H3) \Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind Abst) t) (CHead d1
261 (Bind Abbr) u))).(\lambda (H5: (eq C (CHead c3 (Bind Abbr) u0) c2)).((let H6
262 \def (eq_ind C (CHead c0 (Bind Abst) t) (\lambda (e: C).(match e in C return
263 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
264 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
265 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
266 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
267 \Rightarrow False])])) I (CHead d1 (Bind Abbr) u) H4) in (False_ind ((eq C
268 (CHead c3 (Bind Abbr) u0) c2) \to ((csubt g c0 c3) \to ((ty3 g c3 u0 t) \to
269 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead
270 d2 (Bind Abbr) u))))))) H6)) H5 H2 H3)))]) in (H2 (refl_equal C (CHead d1
271 (Bind Abbr) u)) (refl_equal C c2)))))))))) (\lambda (n0: nat).(\lambda (H:
272 ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
273 C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C
274 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2
275 (Bind Abbr) u)))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H0:
276 (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0: C).(\forall (d1:
277 C).(\forall (u: T).((drop (S n0) O c (CHead d1 (Bind Abbr) u)) \to (ex2 C
278 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c0 (CHead
279 d2 (Bind Abbr) u))))))))) (\lambda (n1: nat).(\lambda (d1: C).(\lambda (u:
280 T).(\lambda (H1: (drop (S n0) O (CSort n1) (CHead d1 (Bind Abbr) u))).(let H2
281 \def (match H1 in drop return (\lambda (n2: nat).(\lambda (n3: nat).(\lambda
282 (c: C).(\lambda (c0: C).(\lambda (_: (drop n2 n3 c c0)).((eq nat n2 (S n0))
283 \to ((eq nat n3 O) \to ((eq C c (CSort n1)) \to ((eq C c0 (CHead d1 (Bind
284 Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
285 (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))))))))))) with [(drop_refl c)
286 \Rightarrow (\lambda (H2: (eq nat O (S n0))).(\lambda (H3: (eq nat O
287 O)).(\lambda (H4: (eq C c (CSort n1))).(\lambda (H5: (eq C c (CHead d1 (Bind
288 Abbr) u))).((let H6 \def (eq_ind nat O (\lambda (e: nat).(match e in nat
289 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow
290 False])) I (S n0) H2) in (False_ind ((eq nat O O) \to ((eq C c (CSort n1))
291 \to ((eq C c (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g
292 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr)
293 u))))))) H6)) H3 H4 H5))))) | (drop_drop k h c e H2 u0) \Rightarrow (\lambda
294 (H3: (eq nat (S h) (S n0))).(\lambda (H4: (eq nat O O)).(\lambda (H5: (eq C
295 (CHead c k u0) (CSort n1))).(\lambda (H6: (eq C e (CHead d1 (Bind Abbr)
296 u))).((let H7 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat
297 return (\lambda (_: nat).nat) with [O \Rightarrow h | (S n2) \Rightarrow
298 n2])) (S h) (S n0) H3) in (eq_ind nat n0 (\lambda (n2: nat).((eq nat O O) \to
299 ((eq C (CHead c k u0) (CSort n1)) \to ((eq C e (CHead d1 (Bind Abbr) u)) \to
300 ((drop (r k n2) O c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
301 (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))))))) (\lambda
302 (_: (eq nat O O)).(\lambda (H9: (eq C (CHead c k u0) (CSort n1))).(let H10
303 \def (eq_ind C (CHead c k u0) (\lambda (e0: C).(match e0 in C return (\lambda
304 (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow
305 True])) I (CSort n1) H9) in (False_ind ((eq C e (CHead d1 (Bind Abbr) u)) \to
306 ((drop (r k n0) O c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
307 (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)))))) H10)))) h
308 (sym_eq nat h n0 H7))) H4 H5 H6 H2))))) | (drop_skip k h d c e H2 u0)
309 \Rightarrow (\lambda (H3: (eq nat h (S n0))).(\lambda (H4: (eq nat (S d)
310 O)).(\lambda (H5: (eq C (CHead c k (lift h (r k d) u0)) (CSort n1))).(\lambda
311 (H6: (eq C (CHead e k u0) (CHead d1 (Bind Abbr) u))).(eq_ind nat (S n0)
312 (\lambda (n2: nat).((eq nat (S d) O) \to ((eq C (CHead c k (lift n2 (r k d)
313 u0)) (CSort n1)) \to ((eq C (CHead e k u0) (CHead d1 (Bind Abbr) u)) \to
314 ((drop n2 (r k d) c e) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
315 (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))))))) (\lambda
316 (H7: (eq nat (S d) O)).(let H8 \def (eq_ind nat (S d) (\lambda (e0:
317 nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
318 False | (S _) \Rightarrow True])) I O H7) in (False_ind ((eq C (CHead c k
319 (lift (S n0) (r k d) u0)) (CSort n1)) \to ((eq C (CHead e k u0) (CHead d1
320 (Bind Abbr) u)) \to ((drop (S n0) (r k d) c e) \to (ex2 C (\lambda (d2:
321 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
322 (Bind Abbr) u))))))) H8))) h (sym_eq nat h (S n0) H3) H4 H5 H6 H2)))))]) in
323 (H2 (refl_equal nat (S n0)) (refl_equal nat O) (refl_equal C (CSort n1))
324 (refl_equal C (CHead d1 (Bind Abbr) u)))))))) (\lambda (c0: C).(\lambda (c3:
325 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall
326 (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
327 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr)
328 u))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall
329 (d1: C).(\forall (u0: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1 (Bind
330 Abbr) u0)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
331 C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abbr) u0))))))))) (\lambda
332 (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H3: (drop
333 (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abbr) u0))).(ex2_ind C
334 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
335 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
336 C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda
337 (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5: (drop n0 O c3 (CHead x
338 (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
339 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0))) x H4
340 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u0) H5 u))))) (H c0 c3 H1 d1
341 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Bind Abbr) u0) u n0 H3))))))))
342 (\lambda (f: F).(\lambda (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda
343 (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abbr)
344 u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
345 n0) O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2))
346 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr)
347 u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5: (drop (S
348 n0) O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1
349 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
350 Abbr) u0))) x H4 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abbr) u0) H5 u)))))
351 (H2 d1 u0 (drop_gen_drop (Flat f) c0 (CHead d1 (Bind Abbr) u0) u n0
352 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g
353 c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0
354 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
355 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda
356 (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
357 T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S n0) O (CHead c0
358 (Bind Void) u1) (CHead d1 (Bind Abbr) u))).(ex2_ind C (\lambda (d2: C).(csubt
359 g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr) u))) (ex2 C
360 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
361 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (x: C).(\lambda (H5: (csubt
362 g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Bind Abbr) u))).(ex_intro2 C
363 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
364 (Bind b) u2) (CHead d2 (Bind Abbr) u))) x H5 (drop_drop (Bind b) n0 c3 (CHead
365 x (Bind Abbr) u) H6 u2))))) (H c0 c3 H1 d1 u (drop_gen_drop (Bind Void) c0
366 (CHead d1 (Bind Abbr) u) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda
367 (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1:
368 C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C
369 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead
370 d2 (Bind Abbr) u))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g
371 c3 u t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H4: (drop (S n0) O
372 (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abbr) u0))).(ex2_ind C (\lambda (d2:
373 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr)
374 u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0)
375 O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (x:
376 C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Bind
377 Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
378 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))) x H5
379 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind Abbr) u0) H6 u))))) (H c0 c3 H1
380 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Bind Abbr) u0) t n0
381 H4))))))))))))) c1 c2 H0)))))) n)).
383 theorem csubt_drop_abst:
384 \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
385 c1 c2) \to (\forall (d1: C).(\forall (t: T).((drop n O c1 (CHead d1 (Bind
386 Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
387 C).(drop n O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
388 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n
389 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
392 \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
393 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (t:
394 T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
395 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abst)
396 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
397 (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda
398 (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))))) (\lambda (c1: C).(\lambda
399 (c2: C).(\lambda (H: (csubt g c1 c2)).(\lambda (d1: C).(\lambda (t:
400 T).(\lambda (H0: (drop O O c1 (CHead d1 (Bind Abst) t))).(let H1 \def (eq_ind
401 C c1 (\lambda (c: C).(csubt g c c2)) H (CHead d1 (Bind Abst) t)
402 (drop_gen_refl c1 (CHead d1 (Bind Abst) t) H0)) in (let H2 \def (match H1 in
403 csubt return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csubt ? c
404 c0)).((eq C c (CHead d1 (Bind Abst) t)) \to ((eq C c0 c2) \to (or (ex2 C
405 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2
406 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
407 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr)
408 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) with
409 [(csubt_sort n0) \Rightarrow (\lambda (H2: (eq C (CSort n0) (CHead d1 (Bind
410 Abst) t))).(\lambda (H3: (eq C (CSort n0) c2)).((let H4 \def (eq_ind C (CSort
411 n0) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort
412 _) \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind
413 Abst) t) H2) in (False_ind ((eq C (CSort n0) c2) \to (or (ex2 C (\lambda (d2:
414 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t))))
415 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
416 C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
417 C).(\lambda (u: T).(ty3 g d2 u t)))))) H4)) H3))) | (csubt_head c0 c3 H2 k u)
418 \Rightarrow (\lambda (H3: (eq C (CHead c0 k u) (CHead d1 (Bind Abst)
419 t))).(\lambda (H4: (eq C (CHead c3 k u) c2)).((let H5 \def (f_equal C T
420 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
421 \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k u) (CHead d1
422 (Bind Abst) t) H3) in ((let H6 \def (f_equal C K (\lambda (e: C).(match e in
423 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
424 \Rightarrow k0])) (CHead c0 k u) (CHead d1 (Bind Abst) t) H3) in ((let H7
425 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
426 with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k
427 u) (CHead d1 (Bind Abst) t) H3) in (eq_ind C d1 (\lambda (c: C).((eq K k
428 (Bind Abst)) \to ((eq T u t) \to ((eq C (CHead c3 k u) c2) \to ((csubt g c
429 c3) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O
430 O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
431 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop O O c2 (CHead d2
432 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))))))))
433 (\lambda (H8: (eq K k (Bind Abst))).(eq_ind K (Bind Abst) (\lambda (k0:
434 K).((eq T u t) \to ((eq C (CHead c3 k0 u) c2) \to ((csubt g d1 c3) \to (or
435 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead
436 d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
437 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop O O c2 (CHead d2 (Bind Abbr)
438 u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))))))) (\lambda
439 (H9: (eq T u t)).(eq_ind T t (\lambda (t0: T).((eq C (CHead c3 (Bind Abst)
440 t0) c2) \to ((csubt g d1 c3) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
441 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
442 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
443 T).(drop O O c2 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
444 T).(ty3 g d2 u0 t)))))))) (\lambda (H10: (eq C (CHead c3 (Bind Abst) t)
445 c2)).(eq_ind C (CHead c3 (Bind Abst) t) (\lambda (c: C).((csubt g d1 c3) \to
446 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c
447 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
448 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop O O c (CHead d2
449 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))))
450 (\lambda (H11: (csubt g d1 c3)).(or_introl (ex2 C (\lambda (d2: C).(csubt g
451 d1 d2)) (\lambda (d2: C).(drop O O (CHead c3 (Bind Abst) t) (CHead d2 (Bind
452 Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
453 (\lambda (d2: C).(\lambda (u0: T).(drop O O (CHead c3 (Bind Abst) t) (CHead
454 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
455 (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O
456 (CHead c3 (Bind Abst) t) (CHead d2 (Bind Abst) t))) c3 H11 (drop_refl (CHead
457 c3 (Bind Abst) t))))) c2 H10)) u (sym_eq T u t H9))) k (sym_eq K k (Bind
458 Abst) H8))) c0 (sym_eq C c0 d1 H7))) H6)) H5)) H4 H2))) | (csubt_void c0 c3
459 H2 b H3 u1 u2) \Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind Void) u1)
460 (CHead d1 (Bind Abst) t))).(\lambda (H5: (eq C (CHead c3 (Bind b) u2)
461 c2)).((let H6 \def (eq_ind C (CHead c0 (Bind Void) u1) (\lambda (e: C).(match
462 e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
463 (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
464 [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
465 \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat
466 _) \Rightarrow False])])) I (CHead d1 (Bind Abst) t) H4) in (False_ind ((eq C
467 (CHead c3 (Bind b) u2) c2) \to ((csubt g c0 c3) \to ((not (eq B b Void)) \to
468 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2
469 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
470 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c2 (CHead d2
471 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))) H6))
472 H5 H2 H3))) | (csubt_abst c0 c3 H2 u t0 H3) \Rightarrow (\lambda (H4: (eq C
473 (CHead c0 (Bind Abst) t0) (CHead d1 (Bind Abst) t))).(\lambda (H5: (eq C
474 (CHead c3 (Bind Abbr) u) c2)).((let H6 \def (f_equal C T (\lambda (e:
475 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t0 |
476 (CHead _ _ t1) \Rightarrow t1])) (CHead c0 (Bind Abst) t0) (CHead d1 (Bind
477 Abst) t) H4) in ((let H7 \def (f_equal C C (\lambda (e: C).(match e in C
478 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _)
479 \Rightarrow c])) (CHead c0 (Bind Abst) t0) (CHead d1 (Bind Abst) t) H4) in
480 (eq_ind C d1 (\lambda (c: C).((eq T t0 t) \to ((eq C (CHead c3 (Bind Abbr) u)
481 c2) \to ((csubt g c c3) \to ((ty3 g c3 u t0) \to (or (ex2 C (\lambda (d2:
482 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t))))
483 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
484 C).(\lambda (u0: T).(drop O O c2 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
485 C).(\lambda (u0: T).(ty3 g d2 u0 t)))))))))) (\lambda (H8: (eq T t0
486 t)).(eq_ind T t (\lambda (t1: T).((eq C (CHead c3 (Bind Abbr) u) c2) \to
487 ((csubt g d1 c3) \to ((ty3 g c3 u t1) \to (or (ex2 C (\lambda (d2: C).(csubt
488 g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C
489 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
490 C).(\lambda (u0: T).(drop O O c2 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
491 C).(\lambda (u0: T).(ty3 g d2 u0 t))))))))) (\lambda (H9: (eq C (CHead c3
492 (Bind Abbr) u) c2)).(eq_ind C (CHead c3 (Bind Abbr) u) (\lambda (c:
493 C).((csubt g d1 c3) \to ((ty3 g c3 u t) \to (or (ex2 C (\lambda (d2:
494 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abst) t))))
495 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
496 C).(\lambda (u0: T).(drop O O c (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
497 C).(\lambda (u0: T).(ty3 g d2 u0 t)))))))) (\lambda (H10: (csubt g d1
498 c3)).(\lambda (H11: (ty3 g c3 u t)).(or_intror (ex2 C (\lambda (d2: C).(csubt
499 g d1 d2)) (\lambda (d2: C).(drop O O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
500 Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
501 (\lambda (d2: C).(\lambda (u0: T).(drop O O (CHead c3 (Bind Abbr) u) (CHead
502 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
503 (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
504 (d2: C).(\lambda (u0: T).(drop O O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
505 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) c3 u H10
506 (drop_refl (CHead c3 (Bind Abbr) u)) H11)))) c2 H9)) t0 (sym_eq T t0 t H8)))
507 c0 (sym_eq C c0 d1 H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal C (CHead d1
508 (Bind Abst) t)) (refl_equal C c2)))))))))) (\lambda (n0: nat).(\lambda (H:
509 ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
510 C).(\forall (t: T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C
511 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2
512 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
513 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr)
514 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))))))))))).(\lambda
515 (c1: C).(\lambda (c2: C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda
516 (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (t: T).((drop (S n0) O c
517 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
518 (\lambda (d2: C).(drop (S n0) O c0 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
519 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
520 (u: T).(drop (S n0) O c0 (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
521 C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (n1: nat).(\lambda (d1:
522 C).(\lambda (t: T).(\lambda (H1: (drop (S n0) O (CSort n1) (CHead d1 (Bind
523 Abst) t))).(let H2 \def (match H1 in drop return (\lambda (n2: nat).(\lambda
524 (n3: nat).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop n2 n3 c
525 c0)).((eq nat n2 (S n0)) \to ((eq nat n3 O) \to ((eq C c (CSort n1)) \to ((eq
526 C c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1
527 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t))))
528 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
529 C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
530 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))))))) with [(drop_refl
531 c) \Rightarrow (\lambda (H2: (eq nat O (S n0))).(\lambda (H3: (eq nat O
532 O)).(\lambda (H4: (eq C c (CSort n1))).(\lambda (H5: (eq C c (CHead d1 (Bind
533 Abst) t))).((let H6 \def (eq_ind nat O (\lambda (e: nat).(match e in nat
534 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow
535 False])) I (S n0) H2) in (False_ind ((eq nat O O) \to ((eq C c (CSort n1))
536 \to ((eq C c (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt
537 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abst)
538 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
539 (d2: C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
540 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))) H6)) H3 H4 H5))))) |
541 (drop_drop k h c e H2 u) \Rightarrow (\lambda (H3: (eq nat (S h) (S
542 n0))).(\lambda (H4: (eq nat O O)).(\lambda (H5: (eq C (CHead c k u) (CSort
543 n1))).(\lambda (H6: (eq C e (CHead d1 (Bind Abst) t))).((let H7 \def (f_equal
544 nat nat (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).nat)
545 with [O \Rightarrow h | (S n2) \Rightarrow n2])) (S h) (S n0) H3) in (eq_ind
546 nat n0 (\lambda (n2: nat).((eq nat O O) \to ((eq C (CHead c k u) (CSort n1))
547 \to ((eq C e (CHead d1 (Bind Abst) t)) \to ((drop (r k n2) O c e) \to (or
548 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
549 (CSort n1) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda
550 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
551 (CSort n1) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
552 T).(ty3 g d2 u0 t)))))))))) (\lambda (_: (eq nat O O)).(\lambda (H9: (eq C
553 (CHead c k u) (CSort n1))).(let H10 \def (eq_ind C (CHead c k u) (\lambda
554 (e0: C).(match e0 in C return (\lambda (_: C).Prop) with [(CSort _)
555 \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n1) H9) in
556 (False_ind ((eq C e (CHead d1 (Bind Abst) t)) \to ((drop (r k n0) O c e) \to
557 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
558 (CSort n1) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda
559 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
560 (CSort n1) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
561 T).(ty3 g d2 u0 t))))))) H10)))) h (sym_eq nat h n0 H7))) H4 H5 H6 H2))))) |
562 (drop_skip k h d c e H2 u) \Rightarrow (\lambda (H3: (eq nat h (S
563 n0))).(\lambda (H4: (eq nat (S d) O)).(\lambda (H5: (eq C (CHead c k (lift h
564 (r k d) u)) (CSort n1))).(\lambda (H6: (eq C (CHead e k u) (CHead d1 (Bind
565 Abst) t))).(eq_ind nat (S n0) (\lambda (n2: nat).((eq nat (S d) O) \to ((eq C
566 (CHead c k (lift n2 (r k d) u)) (CSort n1)) \to ((eq C (CHead e k u) (CHead
567 d1 (Bind Abst) t)) \to ((drop n2 (r k d) c e) \to (or (ex2 C (\lambda (d2:
568 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
569 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
570 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CSort n1) (CHead d2
571 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))))))))
572 (\lambda (H7: (eq nat (S d) O)).(let H8 \def (eq_ind nat (S d) (\lambda (e0:
573 nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
574 False | (S _) \Rightarrow True])) I O H7) in (False_ind ((eq C (CHead c k
575 (lift (S n0) (r k d) u)) (CSort n1)) \to ((eq C (CHead e k u) (CHead d1 (Bind
576 Abst) t)) \to ((drop (S n0) (r k d) c e) \to (or (ex2 C (\lambda (d2:
577 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
578 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
579 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CSort n1) (CHead d2
580 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))))))
581 H8))) h (sym_eq nat h (S n0) H3) H4 H5 H6 H2)))))]) in (H2 (refl_equal nat (S
582 n0)) (refl_equal nat O) (refl_equal C (CSort n1)) (refl_equal C (CHead d1
583 (Bind Abst) t)))))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt
584 g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (t: T).((drop (S n0) O c0
585 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
586 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
587 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
588 (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
589 C).(\lambda (u: T).(ty3 g d2 u t)))))))))).(\lambda (k: K).(K_ind (\lambda
590 (k0: K).(\forall (u: T).(\forall (d1: C).(\forall (t: T).((drop (S n0) O
591 (CHead c0 k0 u) (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
592 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2
593 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
594 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 k0 u) (CHead
595 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
596 t)))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda (t:
597 T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abst)
598 t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
599 n0 O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
600 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead
601 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
602 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
603 (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
604 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
605 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
606 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (H4: (ex2 C (\lambda (d2:
607 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst)
608 t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0
609 O c3 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
610 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst)
611 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
612 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
613 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda
614 (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x
615 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
616 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t))))
617 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
618 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
619 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex_intro2
620 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
621 (Bind b) u) (CHead d2 (Bind Abst) t))) x H5 (drop_drop (Bind b) n0 c3 (CHead
622 x (Bind Abst) t) H6 u)))))) H4)) (\lambda (H4: (ex3_2 C T (\lambda (d2:
623 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
624 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g
625 d2 u0 t))))).(ex3_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
626 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr)
627 u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C
628 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
629 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda
630 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
631 (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda
632 (u0: T).(ty3 g d2 u0 t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5:
633 (csubt g d1 x0)).(\lambda (H6: (drop n0 O c3 (CHead x0 (Bind Abbr)
634 x1))).(\lambda (H7: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2:
635 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
636 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
637 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
638 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
639 T).(ty3 g d2 u0 t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_:
640 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
641 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
642 T).(ty3 g d2 u0 t))) x0 x1 H5 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr)
643 x1) H6 u) H7))))))) H4)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind b) c0 (CHead
644 d1 (Bind Abst) t) u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda
645 (d1: C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u)
646 (CHead d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2))
647 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
648 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
649 (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
650 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (or (ex2 C (\lambda (d2: C).(csubt g
651 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
652 Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
653 (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead
654 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))
655 (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
656 (S n0) O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g
657 d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))) (or
658 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
659 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
660 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
661 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
662 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt
663 g d1 x)).(\lambda (H6: (drop (S n0) O c3 (CHead x (Bind Abst) t))).(or_introl
664 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
665 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
666 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
667 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
668 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex_intro2 C (\lambda (d2: C).(csubt g
669 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
670 Abst) t))) x H5 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abst) t) H6 u))))))
671 H4)) (\lambda (H4: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
672 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind
673 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))).(ex3_2_ind
674 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
675 C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda
676 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda (d2: C).(csubt
677 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2
678 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
679 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u)
680 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
681 t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (csubt g d1
682 x0)).(\lambda (H6: (drop (S n0) O c3 (CHead x0 (Bind Abbr) x1))).(\lambda
683 (H7: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2))
684 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst)
685 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
686 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
687 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
688 (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
689 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
690 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) x0 x1 H5
691 (drop_drop (Flat f) n0 c3 (CHead x0 (Bind Abbr) x1) H6 u) H7))))))) H4)) (H2
692 d1 t (drop_gen_drop (Flat f) c0 (CHead d1 (Bind Abst) t) u n0 H3))))))))
693 k)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0
694 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t: T).((drop (S n0) O c0 (CHead
695 d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
696 (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
697 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
698 T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda
699 (u: T).(ty3 g d2 u t)))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b
700 Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (t:
701 T).(\lambda (H4: (drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind
702 Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
703 C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
704 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
705 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
706 d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
707 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C
708 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
709 C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind
710 Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H5:
711 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3
712 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
713 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda
714 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
715 u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
716 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
717 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
718 T).(ty3 g d2 u t))))) (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda
719 (H7: (drop n0 O c3 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2:
720 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2)
721 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
722 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
723 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
724 T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
725 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t))) x H6
726 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abst) t) H7 u2)))))) H5)) (\lambda
727 (H5: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
728 (d2: C).(\lambda (u: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda
729 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex3_2_ind C T (\lambda (d2:
730 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
731 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
732 d2 u t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
733 (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T
734 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
735 (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u))))
736 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x0: C).(\lambda
737 (x1: T).(\lambda (H6: (csubt g d1 x0)).(\lambda (H7: (drop n0 O c3 (CHead x0
738 (Bind Abbr) x1))).(\lambda (H8: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda
739 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
740 u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
741 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
742 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
743 T).(ty3 g d2 u t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt
744 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b)
745 u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
746 t))) x0 x1 H6 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H7 u2)
747 H8))))))) H5)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind Void) c0 (CHead d1 (Bind
748 Abst) t) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
749 (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t: T).((drop
750 (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt
751 g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))
752 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
753 C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda
754 (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))).(\lambda (u: T).(\lambda (t:
755 T).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (t0: T).(\lambda
756 (H4: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abst)
757 t0))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
758 n0 O c3 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
759 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead
760 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))
761 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
762 (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda
763 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
764 T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))))
765 (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))) (\lambda (H5: (ex2 C
766 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
767 (Bind Abst) t0))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
768 (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t0))) (or (ex2 C (\lambda (d2:
769 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
770 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
771 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
772 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
773 T).(ty3 g d2 u0 t0))))) (\lambda (x: C).(\lambda (H6: (csubt g d1
774 x)).(\lambda (H7: (drop n0 O c3 (CHead x (Bind Abst) t0))).(or_introl (ex2 C
775 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
776 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2:
777 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
778 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
779 C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex_intro2 C (\lambda (d2: C).(csubt
780 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2
781 (Bind Abst) t0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind Abst) t0)
782 H7 u)))))) H5)) (\lambda (H5: (ex3_2 C T (\lambda (d2: C).(\lambda (_:
783 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead
784 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
785 t0))))).(ex3_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
786 (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))))
787 (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))) (or (ex2 C (\lambda (d2:
788 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
789 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
790 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
791 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
792 T).(ty3 g d2 u0 t0))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6:
793 (csubt g d1 x0)).(\lambda (H7: (drop n0 O c3 (CHead x0 (Bind Abbr)
794 x1))).(\lambda (H8: (ty3 g x0 x1 t0)).(or_intror (ex2 C (\lambda (d2:
795 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
796 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
797 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
798 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
799 T).(ty3 g d2 u0 t0)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_:
800 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
801 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
802 T).(ty3 g d2 u0 t0))) x0 x1 H6 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind
803 Abbr) x1) H7 u) H8))))))) H5)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst)
804 c0 (CHead d1 (Bind Abst) t0) t n0 H4))))))))))))) c1 c2 H0)))))) n)).
projects / helm.git / blob