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