]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / arity / fwd.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "LambdaDelta-1/arity/defs.ma".
18
19 include "LambdaDelta-1/leq/asucc.ma".
20
21 include "LambdaDelta-1/leq/fwd.ma".
22
23 include "LambdaDelta-1/getl/drop.ma".
24
25 theorem arity_gen_sort:
26  \forall (g: G).(\forall (c: C).(\forall (n: nat).(\forall (a: A).((arity g c 
27 (TSort n) a) \to (leq g a (ASort O n))))))
28 \def
29  \lambda (g: G).(\lambda (c: C).(\lambda (n: nat).(\lambda (a: A).(\lambda 
30 (H: (arity g c (TSort n) a)).(insert_eq T (TSort n) (\lambda (t: T).(arity g 
31 c t a)) (\lambda (_: T).(leq g a (ASort O n))) (\lambda (y: T).(\lambda (H0: 
32 (arity g c y a)).(arity_ind g (\lambda (_: C).(\lambda (t: T).(\lambda (a0: 
33 A).((eq T t (TSort n)) \to (leq g a0 (ASort O n)))))) (\lambda (_: 
34 C).(\lambda (n0: nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def 
35 (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with 
36 [(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _) 
37 \Rightarrow n0])) (TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1: 
38 nat).(leq g (ASort O n1) (ASort O n))) (leq_refl g (ASort O n)) n0 H2))))) 
39 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
40 (_: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity 
41 g d u a0)).(\lambda (_: (((eq T u (TSort n)) \to (leq g a0 (ASort O 
42 n))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T 
43 (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with 
44 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) 
45 \Rightarrow False])) I (TSort n) H4) in (False_ind (leq g a0 (ASort O n)) 
46 H5))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: 
47 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abst) u))).(\lambda (a0: 
48 A).(\lambda (_: (arity g d u (asucc g a0))).(\lambda (_: (((eq T u (TSort n)) 
49 \to (leq g (asucc g a0) (ASort O n))))).(\lambda (H4: (eq T (TLRef i) (TSort 
50 n))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
51 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
52 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in 
53 (False_ind (leq g a0 (ASort O n)) H5))))))))))) (\lambda (b: B).(\lambda (_: 
54 (not (eq B b Abst))).(\lambda (c0: C).(\lambda (u: T).(\lambda (a1: 
55 A).(\lambda (_: (arity g c0 u a1)).(\lambda (_: (((eq T u (TSort n)) \to (leq 
56 g a1 (ASort O n))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g 
57 (CHead c0 (Bind b) u) t a2)).(\lambda (_: (((eq T t (TSort n)) \to (leq g a2 
58 (ASort O n))))).(\lambda (H6: (eq T (THead (Bind b) u t) (TSort n))).(let H7 
59 \def (eq_ind T (THead (Bind b) u t) (\lambda (ee: T).(match ee in T return 
60 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
61 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H6) in 
62 (False_ind (leq g a2 (ASort O n)) H7)))))))))))))) (\lambda (c0: C).(\lambda 
63 (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u (asucc g a1))).(\lambda 
64 (_: (((eq T u (TSort n)) \to (leq g (asucc g a1) (ASort O n))))).(\lambda (t: 
65 T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t 
66 a2)).(\lambda (_: (((eq T t (TSort n)) \to (leq g a2 (ASort O n))))).(\lambda 
67 (H5: (eq T (THead (Bind Abst) u t) (TSort n))).(let H6 \def (eq_ind T (THead 
68 (Bind Abst) u t) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) 
69 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ 
70 _) \Rightarrow True])) I (TSort n) H5) in (False_ind (leq g (AHead a1 a2) 
71 (ASort O n)) H6)))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a1: 
72 A).(\lambda (_: (arity g c0 u a1)).(\lambda (_: (((eq T u (TSort n)) \to (leq 
73 g a1 (ASort O n))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g 
74 c0 t (AHead a1 a2))).(\lambda (_: (((eq T t (TSort n)) \to (leq g (AHead a1 
75 a2) (ASort O n))))).(\lambda (H5: (eq T (THead (Flat Appl) u t) (TSort 
76 n))).(let H6 \def (eq_ind T (THead (Flat Appl) u t) (\lambda (ee: T).(match 
77 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
78 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) 
79 H5) in (False_ind (leq g a2 (ASort O n)) H6)))))))))))) (\lambda (c0: 
80 C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c0 u (asucc g 
81 a0))).(\lambda (_: (((eq T u (TSort n)) \to (leq g (asucc g a0) (ASort O 
82 n))))).(\lambda (t: T).(\lambda (_: (arity g c0 t a0)).(\lambda (_: (((eq T t 
83 (TSort n)) \to (leq g a0 (ASort O n))))).(\lambda (H5: (eq T (THead (Flat 
84 Cast) u t) (TSort n))).(let H6 \def (eq_ind T (THead (Flat Cast) u t) 
85 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
86 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
87 True])) I (TSort n) H5) in (False_ind (leq g a0 (ASort O n)) H6))))))))))) 
88 (\lambda (c0: C).(\lambda (t: T).(\lambda (a1: A).(\lambda (H1: (arity g c0 t 
89 a1)).(\lambda (H2: (((eq T t (TSort n)) \to (leq g a1 (ASort O 
90 n))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T t 
91 (TSort n))).(let H5 \def (f_equal T T (\lambda (e: T).e) t (TSort n) H4) in 
92 (let H6 \def (eq_ind T t (\lambda (t0: T).((eq T t0 (TSort n)) \to (leq g a1 
93 (ASort O n)))) H2 (TSort n) H5) in (let H7 \def (eq_ind T t (\lambda (t0: 
94 T).(arity g c0 t0 a1)) H1 (TSort n) H5) in (leq_trans g a2 a1 (leq_sym g a1 
95 a2 H3) (ASort O n) (H6 (refl_equal T (TSort n))))))))))))))) c y a H0))) 
96 H))))).
97
98 theorem arity_gen_lref:
99  \forall (g: G).(\forall (c: C).(\forall (i: nat).(\forall (a: A).((arity g c 
100 (TLRef i) a) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c 
101 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u a)))) 
102 (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c (CHead d (Bind Abst) 
103 u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a))))))))))
104 \def
105  \lambda (g: G).(\lambda (c: C).(\lambda (i: nat).(\lambda (a: A).(\lambda 
106 (H: (arity g c (TLRef i) a)).(insert_eq T (TLRef i) (\lambda (t: T).(arity g 
107 c t a)) (\lambda (_: T).(or (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl 
108 i c (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
109 a)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c (CHead d (Bind 
110 Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a))))))) 
111 (\lambda (y: T).(\lambda (H0: (arity g c y a)).(arity_ind g (\lambda (c0: 
112 C).(\lambda (t: T).(\lambda (a0: A).((eq T t (TLRef i)) \to (or (ex2_2 C T 
113 (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) 
114 (\lambda (d: C).(\lambda (u: T).(arity g d u a0)))) (ex2_2 C T (\lambda (d: 
115 C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) (\lambda (d: 
116 C).(\lambda (u: T).(arity g d u (asucc g a0)))))))))) (\lambda (c0: 
117 C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) (TLRef i))).(let H2 \def 
118 (eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_: 
119 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
120 (THead _ _ _) \Rightarrow False])) I (TLRef i) H1) in (False_ind (or (ex2_2 C 
121 T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) 
122 (\lambda (d: C).(\lambda (u: T).(arity g d u (ASort O n))))) (ex2_2 C T 
123 (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) 
124 (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g (ASort O n))))))) 
125 H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i0: 
126 nat).(\lambda (H1: (getl i0 c0 (CHead d (Bind Abbr) u))).(\lambda (a0: 
127 A).(\lambda (H2: (arity g d u a0)).(\lambda (_: (((eq T u (TLRef i)) \to (or 
128 (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abbr) 
129 u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T 
130 (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abst) u0)))) 
131 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g 
132 a0))))))))).(\lambda (H4: (eq T (TLRef i0) (TLRef i))).(let H5 \def (f_equal 
133 T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort 
134 _) \Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) 
135 (TLRef i0) (TLRef i) H4) in (let H6 \def (eq_ind nat i0 (\lambda (n: 
136 nat).(getl n c0 (CHead d (Bind Abbr) u))) H1 i H5) in (or_introl (ex2_2 C T 
137 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) 
138 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda 
139 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda 
140 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2_intro C T 
141 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) 
142 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0))) d u H6 H2))))))))))))) 
143 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i0: nat).(\lambda 
144 (H1: (getl i0 c0 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (H2: 
145 (arity g d u (asucc g a0))).(\lambda (_: (((eq T u (TLRef i)) \to (or (ex2_2 
146 C T (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abbr) u0)))) 
147 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2 C T 
148 (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abst) u0)))) 
149 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g (asucc g 
150 a0)))))))))).(\lambda (H4: (eq T (TLRef i0) (TLRef i))).(let H5 \def (f_equal 
151 T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort 
152 _) \Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) 
153 (TLRef i0) (TLRef i) H4) in (let H6 \def (eq_ind nat i0 (\lambda (n: 
154 nat).(getl n c0 (CHead d (Bind Abst) u))) H1 i H5) in (or_intror (ex2_2 C T 
155 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) 
156 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda 
157 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda 
158 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2_intro C T 
159 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) 
160 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0)))) d u H6 
161 H2))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
162 (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u 
163 a1)).(\lambda (_: (((eq T u (TLRef i)) \to (or (ex2_2 C T (\lambda (d: 
164 C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: 
165 C).(\lambda (u0: T).(arity g d u0 a1)))) (ex2_2 C T (\lambda (d: C).(\lambda 
166 (u0: T).(getl i c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: 
167 T).(arity g d u0 (asucc g a1))))))))).(\lambda (t: T).(\lambda (a2: 
168 A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t a2)).(\lambda (_: (((eq T t 
169 (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i (CHead 
170 c0 (Bind b) u) (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: 
171 T).(arity g d u0 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i 
172 (CHead c0 (Bind b) u) (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda 
173 (u0: T).(arity g d u0 (asucc g a2))))))))).(\lambda (H6: (eq T (THead (Bind 
174 b) u t) (TLRef i))).(let H7 \def (eq_ind T (THead (Bind b) u t) (\lambda (ee: 
175 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
176 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
177 (TLRef i) H6) in (False_ind (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: 
178 T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: 
179 T).(arity g d u0 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i 
180 c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
181 (asucc g a2)))))) H7)))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda 
182 (a1: A).(\lambda (_: (arity g c0 u (asucc g a1))).(\lambda (_: (((eq T u 
183 (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 
184 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
185 (asucc g a1))))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 
186 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
187 (asucc g (asucc g a1)))))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: 
188 (arity g (CHead c0 (Bind Abst) u) t a2)).(\lambda (_: (((eq T t (TLRef i)) 
189 \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i (CHead c0 (Bind 
190 Abst) u) (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity 
191 g d u0 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i (CHead c0 
192 (Bind Abst) u) (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: 
193 T).(arity g d u0 (asucc g a2))))))))).(\lambda (H5: (eq T (THead (Bind Abst) 
194 u t) (TLRef i))).(let H6 \def (eq_ind T (THead (Bind Abst) u t) (\lambda (ee: 
195 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
196 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
197 (TLRef i) H5) in (False_ind (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: 
198 T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: 
199 T).(arity g d u0 (AHead a1 a2))))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: 
200 T).(getl i c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: 
201 T).(arity g d u0 (asucc g (AHead a1 a2))))))) H6)))))))))))) (\lambda (c0: 
202 C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u a1)).(\lambda 
203 (_: (((eq T u (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: 
204 T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: 
205 T).(arity g d u0 a1)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i 
206 c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
207 (asucc g a1))))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g 
208 c0 t (AHead a1 a2))).(\lambda (_: (((eq T t (TLRef i)) \to (or (ex2_2 C T 
209 (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr) u0)))) 
210 (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (AHead a1 a2))))) (ex2_2 C T 
211 (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abst) u0)))) 
212 (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g (AHead a1 
213 a2)))))))))).(\lambda (H5: (eq T (THead (Flat Appl) u t) (TLRef i))).(let H6 
214 \def (eq_ind T (THead (Flat Appl) u t) (\lambda (ee: T).(match ee in T return 
215 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
216 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i) H5) in 
217 (False_ind (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead 
218 d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 a2)))) 
219 (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abst) 
220 u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g a2)))))) 
221 H6)))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: 
222 (arity g c0 u (asucc g a0))).(\lambda (_: (((eq T u (TLRef i)) \to (or (ex2_2 
223 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr) u0)))) 
224 (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g a0))))) (ex2_2 C T 
225 (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abst) u0)))) 
226 (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g (asucc g 
227 a0)))))))))).(\lambda (t: T).(\lambda (_: (arity g c0 t a0)).(\lambda (_: 
228 (((eq T t (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: 
229 T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: 
230 T).(arity g d u0 a0)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i 
231 c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
232 (asucc g a0))))))))).(\lambda (H5: (eq T (THead (Flat Cast) u t) (TLRef 
233 i))).(let H6 \def (eq_ind T (THead (Flat Cast) u t) (\lambda (ee: T).(match 
234 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
235 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i) 
236 H5) in (False_ind (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 
237 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 
238 a0)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind 
239 Abst) u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g a0)))))) 
240 H6))))))))))) (\lambda (c0: C).(\lambda (t: T).(\lambda (a1: A).(\lambda (H1: 
241 (arity g c0 t a1)).(\lambda (H2: (((eq T t (TLRef i)) \to (or (ex2_2 C T 
242 (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) 
243 (\lambda (d: C).(\lambda (u: T).(arity g d u a1)))) (ex2_2 C T (\lambda (d: 
244 C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) (\lambda (d: 
245 C).(\lambda (u: T).(arity g d u (asucc g a1))))))))).(\lambda (a2: 
246 A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T t (TLRef i))).(let H5 
247 \def (f_equal T T (\lambda (e: T).e) t (TLRef i) H4) in (let H6 \def (eq_ind 
248 T t (\lambda (t0: T).((eq T t0 (TLRef i)) \to (or (ex2_2 C T (\lambda (d: 
249 C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) (\lambda (d: 
250 C).(\lambda (u: T).(arity g d u a1)))) (ex2_2 C T (\lambda (d: C).(\lambda 
251 (u: T).(getl i c0 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: 
252 T).(arity g d u (asucc g a1)))))))) H2 (TLRef i) H5) in (let H7 \def (eq_ind 
253 T t (\lambda (t0: T).(arity g c0 t0 a1)) H1 (TLRef i) H5) in (let H8 \def (H6 
254 (refl_equal T (TLRef i))) in (or_ind (ex2_2 C T (\lambda (d: C).(\lambda (u: 
255 T).(getl i c0 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: 
256 T).(arity g d u a1)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
257 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
258 (asucc g a1))))) (or (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
259 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
260 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind 
261 Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a2)))))) 
262 (\lambda (H9: (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d 
263 (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
264 a1))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d 
265 (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u a1))) (or 
266 (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) 
267 u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u a2)))) (ex2_2 C T (\lambda 
268 (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) (\lambda (d: 
269 C).(\lambda (u: T).(arity g d u (asucc g a2)))))) (\lambda (x0: C).(\lambda 
270 (x1: T).(\lambda (H10: (getl i c0 (CHead x0 (Bind Abbr) x1))).(\lambda (H11: 
271 (arity g x0 x1 a1)).(or_introl (ex2_2 C T (\lambda (d: C).(\lambda (u: 
272 T).(getl i c0 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: 
273 T).(arity g d u a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
274 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
275 (asucc g a2))))) (ex2_2_intro C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
276 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u a2))) 
277 x0 x1 H10 (arity_repl g x0 x1 a1 H11 a2 H3))))))) H9)) (\lambda (H9: (ex2_2 C 
278 T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) 
279 (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a1)))))).(ex2_2_ind C T 
280 (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) 
281 (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a1)))) (or (ex2_2 C T 
282 (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) 
283 (\lambda (d: C).(\lambda (u: T).(arity g d u a2)))) (ex2_2 C T (\lambda (d: 
284 C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u)))) (\lambda (d: 
285 C).(\lambda (u: T).(arity g d u (asucc g a2)))))) (\lambda (x0: C).(\lambda 
286 (x1: T).(\lambda (H10: (getl i c0 (CHead x0 (Bind Abst) x1))).(\lambda (H11: 
287 (arity g x0 x1 (asucc g a1))).(or_intror (ex2_2 C T (\lambda (d: C).(\lambda 
288 (u: T).(getl i c0 (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: 
289 T).(arity g d u a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
290 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
291 (asucc g a2))))) (ex2_2_intro C T (\lambda (d: C).(\lambda (u: T).(getl i c0 
292 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
293 (asucc g a2)))) x0 x1 H10 (arity_repl g x0 x1 (asucc g a1) H11 (asucc g a2) 
294 (asucc_repl g a1 a2 H3)))))))) H9)) H8))))))))))))) c y a H0))) H))))).
295
296 theorem arity_gen_bind:
297  \forall (b: B).((not (eq B b Abst)) \to (\forall (g: G).(\forall (c: 
298 C).(\forall (u: T).(\forall (t: T).(\forall (a2: A).((arity g c (THead (Bind 
299 b) u t) a2) \to (ex2 A (\lambda (a1: A).(arity g c u a1)) (\lambda (_: 
300 A).(arity g (CHead c (Bind b) u) t a2))))))))))
301 \def
302  \lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (g: G).(\lambda 
303 (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a2: A).(\lambda (H0: (arity 
304 g c (THead (Bind b) u t) a2)).(insert_eq T (THead (Bind b) u t) (\lambda (t0: 
305 T).(arity g c t0 a2)) (\lambda (_: T).(ex2 A (\lambda (a1: A).(arity g c u 
306 a1)) (\lambda (_: A).(arity g (CHead c (Bind b) u) t a2)))) (\lambda (y: 
307 T).(\lambda (H1: (arity g c y a2)).(arity_ind g (\lambda (c0: C).(\lambda 
308 (t0: T).(\lambda (a: A).((eq T t0 (THead (Bind b) u t)) \to (ex2 A (\lambda 
309 (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t 
310 a))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H2: (eq T (TSort n) 
311 (THead (Bind b) u t))).(let H3 \def (eq_ind T (TSort n) (\lambda (ee: 
312 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
313 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I 
314 (THead (Bind b) u t) H2) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u 
315 a1)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t (ASort O n)))) H3))))) 
316 (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda 
317 (_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a: A).(\lambda (_: (arity 
318 g d u0 a)).(\lambda (_: (((eq T u0 (THead (Bind b) u t)) \to (ex2 A (\lambda 
319 (a1: A).(arity g d u a1)) (\lambda (_: A).(arity g (CHead d (Bind b) u) t 
320 a)))))).(\lambda (H5: (eq T (TLRef i) (THead (Bind b) u t))).(let H6 \def 
321 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
322 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
323 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t) H5) in (False_ind 
324 (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 
325 (Bind b) u) t a))) H6))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda 
326 (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abst) 
327 u0))).(\lambda (a: A).(\lambda (_: (arity g d u0 (asucc g a))).(\lambda (_: 
328 (((eq T u0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a1: A).(arity g d u 
329 a1)) (\lambda (_: A).(arity g (CHead d (Bind b) u) t (asucc g 
330 a))))))).(\lambda (H5: (eq T (TLRef i) (THead (Bind b) u t))).(let H6 \def 
331 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
332 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
333 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t) H5) in (False_ind 
334 (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 
335 (Bind b) u) t a))) H6))))))))))) (\lambda (b0: B).(\lambda (H2: (not (eq B b0 
336 Abst))).(\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (H3: 
337 (arity g c0 u0 a1)).(\lambda (H4: (((eq T u0 (THead (Bind b) u t)) \to (ex2 A 
338 (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind 
339 b) u) t a1)))))).(\lambda (t0: T).(\lambda (a0: A).(\lambda (H5: (arity g 
340 (CHead c0 (Bind b0) u0) t0 a0)).(\lambda (H6: (((eq T t0 (THead (Bind b) u 
341 t)) \to (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind b0) u0) u a3)) 
342 (\lambda (_: A).(arity g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t 
343 a0)))))).(\lambda (H7: (eq T (THead (Bind b0) u0 t0) (THead (Bind b) u 
344 t))).(let H8 \def (f_equal T B (\lambda (e: T).(match e in T return (\lambda 
345 (_: T).B) with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead 
346 k _ _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1) 
347 \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) u0 t0) (THead 
348 (Bind b) u t) H7) in ((let H9 \def (f_equal T T (\lambda (e: T).(match e in T 
349 return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) 
350 \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) (THead (Bind b0) u0 t0) 
351 (THead (Bind b) u t) H7) in ((let H10 \def (f_equal T T (\lambda (e: 
352 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | 
353 (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) (THead (Bind b0) 
354 u0 t0) (THead (Bind b) u t) H7) in (\lambda (H11: (eq T u0 u)).(\lambda (H12: 
355 (eq B b0 b)).(let H13 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 (THead 
356 (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind b0) u0) u 
357 a3)) (\lambda (_: A).(arity g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t 
358 a0))))) H6 t H10) in (let H14 \def (eq_ind T t0 (\lambda (t1: T).(arity g 
359 (CHead c0 (Bind b0) u0) t1 a0)) H5 t H10) in (let H15 \def (eq_ind T u0 
360 (\lambda (t1: T).((eq T t (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: 
361 A).(arity g (CHead c0 (Bind b0) t1) u a3)) (\lambda (_: A).(arity g (CHead 
362 (CHead c0 (Bind b0) t1) (Bind b) u) t a0))))) H13 u H11) in (let H16 \def 
363 (eq_ind T u0 (\lambda (t1: T).(arity g (CHead c0 (Bind b0) t1) t a0)) H14 u 
364 H11) in (let H17 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead (Bind b) 
365 u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: A).(arity g 
366 (CHead c0 (Bind b) u) t a1))))) H4 u H11) in (let H18 \def (eq_ind T u0 
367 (\lambda (t1: T).(arity g c0 t1 a1)) H3 u H11) in (let H19 \def (eq_ind B b0 
368 (\lambda (b1: B).((eq T t (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: 
369 A).(arity g (CHead c0 (Bind b1) u) u a3)) (\lambda (_: A).(arity g (CHead 
370 (CHead c0 (Bind b1) u) (Bind b) u) t a0))))) H15 b H12) in (let H20 \def 
371 (eq_ind B b0 (\lambda (b1: B).(arity g (CHead c0 (Bind b1) u) t a0)) H16 b 
372 H12) in (let H21 \def (eq_ind B b0 (\lambda (b1: B).(not (eq B b1 Abst))) H2 
373 b H12) in (ex_intro2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: 
374 A).(arity g (CHead c0 (Bind b) u) t a0)) a1 H18 H20))))))))))))) H9)) 
375 H8)))))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda 
376 (H2: (arity g c0 u0 (asucc g a1))).(\lambda (H3: (((eq T u0 (THead (Bind b) u 
377 t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: A).(arity g 
378 (CHead c0 (Bind b) u) t (asucc g a1))))))).(\lambda (t0: T).(\lambda (a0: 
379 A).(\lambda (H4: (arity g (CHead c0 (Bind Abst) u0) t0 a0)).(\lambda (H5: 
380 (((eq T t0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g (CHead 
381 c0 (Bind Abst) u0) u a3)) (\lambda (_: A).(arity g (CHead (CHead c0 (Bind 
382 Abst) u0) (Bind b) u) t a0)))))).(\lambda (H6: (eq T (THead (Bind Abst) u0 
383 t0) (THead (Bind b) u t))).(let H7 \def (f_equal T B (\lambda (e: T).(match e 
384 in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow Abst | (TLRef _) 
385 \Rightarrow Abst | (THead k _ _) \Rightarrow (match k in K return (\lambda 
386 (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) 
387 (THead (Bind Abst) u0 t0) (THead (Bind b) u t) H6) in ((let H8 \def (f_equal 
388 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
389 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) 
390 (THead (Bind Abst) u0 t0) (THead (Bind b) u t) H6) in ((let H9 \def (f_equal 
391 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
392 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) 
393 (THead (Bind Abst) u0 t0) (THead (Bind b) u t) H6) in (\lambda (H10: (eq T u0 
394 u)).(\lambda (H11: (eq B Abst b)).(let H12 \def (eq_ind T t0 (\lambda (t1: 
395 T).((eq T t1 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g 
396 (CHead c0 (Bind Abst) u0) u a3)) (\lambda (_: A).(arity g (CHead (CHead c0 
397 (Bind Abst) u0) (Bind b) u) t a0))))) H5 t H9) in (let H13 \def (eq_ind T t0 
398 (\lambda (t1: T).(arity g (CHead c0 (Bind Abst) u0) t1 a0)) H4 t H9) in (let 
399 H14 \def (eq_ind T u0 (\lambda (t1: T).((eq T t (THead (Bind b) u t)) \to 
400 (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind Abst) t1) u a3)) (\lambda 
401 (_: A).(arity g (CHead (CHead c0 (Bind Abst) t1) (Bind b) u) t a0))))) H12 u 
402 H10) in (let H15 \def (eq_ind T u0 (\lambda (t1: T).(arity g (CHead c0 (Bind 
403 Abst) t1) t a0)) H13 u H10) in (let H16 \def (eq_ind T u0 (\lambda (t1: 
404 T).((eq T t1 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u 
405 a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t (asucc g a1)))))) H3 u 
406 H10) in (let H17 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 (asucc g 
407 a1))) H2 u H10) in (let H18 \def (eq_ind_r B b (\lambda (b0: B).((eq T t 
408 (THead (Bind b0) u t)) \to (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind 
409 Abst) u) u a3)) (\lambda (_: A).(arity g (CHead (CHead c0 (Bind Abst) u) 
410 (Bind b0) u) t a0))))) H14 Abst H11) in (let H19 \def (eq_ind_r B b (\lambda 
411 (b0: B).((eq T u (THead (Bind b0) u t)) \to (ex2 A (\lambda (a3: A).(arity g 
412 c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b0) u) t (asucc g a1)))))) 
413 H16 Abst H11) in (let H20 \def (eq_ind_r B b (\lambda (b0: B).(not (eq B b0 
414 Abst))) H Abst H11) in (eq_ind B Abst (\lambda (b0: B).(ex2 A (\lambda (a3: 
415 A).(arity g c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b0) u) t 
416 (AHead a1 a0))))) (let H21 \def (match (H20 (refl_equal B Abst)) in False 
417 return (\lambda (_: False).(ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
418 (\lambda (_: A).(arity g (CHead c0 (Bind Abst) u) t (AHead a1 a0))))) with 
419 []) in H21) b H11))))))))))))) H8)) H7)))))))))))) (\lambda (c0: C).(\lambda 
420 (u0: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u0 a1)).(\lambda (_: (((eq 
421 T u0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
422 (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a1)))))).(\lambda (t0: 
423 T).(\lambda (a0: A).(\lambda (_: (arity g c0 t0 (AHead a1 a0))).(\lambda (_: 
424 (((eq T t0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u 
425 a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t (AHead a1 
426 a0))))))).(\lambda (H6: (eq T (THead (Flat Appl) u0 t0) (THead (Bind b) u 
427 t))).(let H7 \def (eq_ind T (THead (Flat Appl) u0 t0) (\lambda (ee: T).(match 
428 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
429 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
430 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
431 True])])) I (THead (Bind b) u t) H6) in (False_ind (ex2 A (\lambda (a3: 
432 A).(arity g c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a0))) 
433 H7)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a: A).(\lambda (_: 
434 (arity g c0 u0 (asucc g a))).(\lambda (_: (((eq T u0 (THead (Bind b) u t)) 
435 \to (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g 
436 (CHead c0 (Bind b) u) t (asucc g a))))))).(\lambda (t0: T).(\lambda (_: 
437 (arity g c0 t0 a)).(\lambda (_: (((eq T t0 (THead (Bind b) u t)) \to (ex2 A 
438 (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 (Bind 
439 b) u) t a)))))).(\lambda (H6: (eq T (THead (Flat Cast) u0 t0) (THead (Bind b) 
440 u t))).(let H7 \def (eq_ind T (THead (Flat Cast) u0 t0) (\lambda (ee: 
441 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
442 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K 
443 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
444 \Rightarrow True])])) I (THead (Bind b) u t) H6) in (False_ind (ex2 A 
445 (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 (Bind 
446 b) u) t a))) H7))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: 
447 A).(\lambda (H2: (arity g c0 t0 a1)).(\lambda (H3: (((eq T t0 (THead (Bind b) 
448 u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: A).(arity g 
449 (CHead c0 (Bind b) u) t a1)))))).(\lambda (a0: A).(\lambda (H4: (leq g a1 
450 a0)).(\lambda (H5: (eq T t0 (THead (Bind b) u t))).(let H6 \def (f_equal T T 
451 (\lambda (e: T).e) t0 (THead (Bind b) u t) H5) in (let H7 \def (eq_ind T t0 
452 (\lambda (t1: T).((eq T t1 (THead (Bind b) u t)) \to (ex2 A (\lambda (a3: 
453 A).(arity g c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t 
454 a1))))) H3 (THead (Bind b) u t) H6) in (let H8 \def (eq_ind T t0 (\lambda 
455 (t1: T).(arity g c0 t1 a1)) H2 (THead (Bind b) u t) H6) in (let H9 \def (H7 
456 (refl_equal T (THead (Bind b) u t))) in (ex2_ind A (\lambda (a3: A).(arity g 
457 c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a1)) (ex2 A 
458 (\lambda (a3: A).(arity g c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind 
459 b) u) t a0))) (\lambda (x: A).(\lambda (H10: (arity g c0 u x)).(\lambda (H11: 
460 (arity g (CHead c0 (Bind b) u) t a1)).(ex_intro2 A (\lambda (a3: A).(arity g 
461 c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a0)) x H10 
462 (arity_repl g (CHead c0 (Bind b) u) t a1 H11 a0 H4))))) H9))))))))))))) c y 
463 a2 H1))) H0)))))))).
464
465 theorem arity_gen_abst:
466  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a: 
467 A).((arity g c (THead (Bind Abst) u t) a) \to (ex3_2 A A (\lambda (a1: 
468 A).(\lambda (a2: A).(eq A a (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
469 A).(arity g c u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
470 (CHead c (Bind Abst) u) t a2)))))))))
471 \def
472  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a: 
473 A).(\lambda (H: (arity g c (THead (Bind Abst) u t) a)).(insert_eq T (THead 
474 (Bind Abst) u t) (\lambda (t0: T).(arity g c t0 a)) (\lambda (_: T).(ex3_2 A 
475 A (\lambda (a1: A).(\lambda (a2: A).(eq A a (AHead a1 a2)))) (\lambda (a1: 
476 A).(\lambda (_: A).(arity g c u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: 
477 A).(arity g (CHead c (Bind Abst) u) t a2))))) (\lambda (y: T).(\lambda (H0: 
478 (arity g c y a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: 
479 A).((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: 
480 A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
481 A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
482 (CHead c0 (Bind Abst) u) t a2)))))))) (\lambda (c0: C).(\lambda (n: 
483 nat).(\lambda (H1: (eq T (TSort n) (THead (Bind Abst) u t))).(let H2 \def 
484 (eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_: 
485 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
486 (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) u t) H1) in 
487 (False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A (ASort O n) 
488 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g 
489 a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t 
490 a2)))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
491 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a0: 
492 A).(\lambda (_: (arity g d u0 a0)).(\lambda (_: (((eq T u0 (THead (Bind Abst) 
493 u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 
494 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g d u (asucc g a1)))) (\lambda 
495 (_: A).(\lambda (a2: A).(arity g (CHead d (Bind Abst) u) t a2))))))).(\lambda 
496 (H4: (eq T (TLRef i) (THead (Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef 
497 i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
498 _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
499 False])) I (THead (Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: 
500 A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
501 A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
502 (CHead c0 (Bind Abst) u) t a2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
503 C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
504 Abst) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 (asucc g 
505 a0))).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A 
506 (\lambda (a1: A).(\lambda (a2: A).(eq A (asucc g a0) (AHead a1 a2)))) 
507 (\lambda (a1: A).(\lambda (_: A).(arity g d u (asucc g a1)))) (\lambda (_: 
508 A).(\lambda (a2: A).(arity g (CHead d (Bind Abst) u) t a2))))))).(\lambda 
509 (H4: (eq T (TLRef i) (THead (Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef 
510 i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
511 _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
512 False])) I (THead (Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: 
513 A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
514 A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
515 (CHead c0 (Bind Abst) u) t a2)))) H5))))))))))) (\lambda (b: B).(\lambda (H1: 
516 (not (eq B b Abst))).(\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: 
517 A).(\lambda (H2: (arity g c0 u0 a1)).(\lambda (H3: (((eq T u0 (THead (Bind 
518 Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead 
519 a2 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
520 (\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
521 a3))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H4: (arity g (CHead c0 
522 (Bind b) u0) t0 a2)).(\lambda (H5: (((eq T t0 (THead (Bind Abst) u t)) \to 
523 (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
524 (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind b) u0) u (asucc g 
525 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind b) 
526 u0) (Bind Abst) u) t a4))))))).(\lambda (H6: (eq T (THead (Bind b) u0 t0) 
527 (THead (Bind Abst) u t))).(let H7 \def (f_equal T B (\lambda (e: T).(match e 
528 in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b | (TLRef _) 
529 \Rightarrow b | (THead k _ _) \Rightarrow (match k in K return (\lambda (_: 
530 K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead 
531 (Bind b) u0 t0) (THead (Bind Abst) u t) H6) in ((let H8 \def (f_equal T T 
532 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
533 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) 
534 (THead (Bind b) u0 t0) (THead (Bind Abst) u t) H6) in ((let H9 \def (f_equal 
535 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
536 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) 
537 (THead (Bind b) u0 t0) (THead (Bind Abst) u t) H6) in (\lambda (H10: (eq T u0 
538 u)).(\lambda (H11: (eq B b Abst)).(let H12 \def (eq_ind T t0 (\lambda (t1: 
539 T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
540 A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
541 A).(arity g (CHead c0 (Bind b) u0) u (asucc g a3)))) (\lambda (_: A).(\lambda 
542 (a4: A).(arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)))))) H5 t 
543 H9) in (let H13 \def (eq_ind T t0 (\lambda (t1: T).(arity g (CHead c0 (Bind 
544 b) u0) t1 a2)) H4 t H9) in (let H14 \def (eq_ind T u0 (\lambda (t1: T).((eq T 
545 t (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: 
546 A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead 
547 c0 (Bind b) t1) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
548 (CHead (CHead c0 (Bind b) t1) (Bind Abst) u) t a4)))))) H12 u H10) in (let 
549 H15 \def (eq_ind T u0 (\lambda (t1: T).(arity g (CHead c0 (Bind b) t1) t a2)) 
550 H13 u H10) in (let H16 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead 
551 (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 
552 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g 
553 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t 
554 a4)))))) H3 u H10) in (let H17 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 
555 t1 a1)) H2 u H10) in (let H18 \def (eq_ind B b (\lambda (b0: B).((eq T t 
556 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq 
557 A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 
558 (Bind b0) u) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
559 (CHead (CHead c0 (Bind b0) u) (Bind Abst) u) t a4)))))) H14 Abst H11) in (let 
560 H19 \def (eq_ind B b (\lambda (b0: B).(arity g (CHead c0 (Bind b0) u) t a2)) 
561 H15 Abst H11) in (let H20 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 
562 Abst))) H1 Abst H11) in (let H21 \def (match (H20 (refl_equal B Abst)) in 
563 False return (\lambda (_: False).(ex3_2 A A (\lambda (a3: A).(\lambda (a4: 
564 A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u 
565 (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind 
566 Abst) u) t a4))))) with []) in H21))))))))))))) H8)) H7)))))))))))))) 
567 (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (H1: (arity g c0 
568 u0 (asucc g a1))).(\lambda (H2: (((eq T u0 (THead (Bind Abst) u t)) \to 
569 (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A (asucc g a1) (AHead a2 
570 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
571 (\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
572 a3))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H3: (arity g (CHead c0 
573 (Bind Abst) u0) t0 a2)).(\lambda (H4: (((eq T t0 (THead (Bind Abst) u t)) \to 
574 (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
575 (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) u0) u (asucc 
576 g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind 
577 Abst) u0) (Bind Abst) u) t a4))))))).(\lambda (H5: (eq T (THead (Bind Abst) 
578 u0 t0) (THead (Bind Abst) u t))).(let H6 \def (f_equal T T (\lambda (e: 
579 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | 
580 (TLRef _) \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) (THead (Bind 
581 Abst) u0 t0) (THead (Bind Abst) u t) H5) in ((let H7 \def (f_equal T T 
582 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
583 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) 
584 (THead (Bind Abst) u0 t0) (THead (Bind Abst) u t) H5) in (\lambda (H8: (eq T 
585 u0 u)).(let H9 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 (THead (Bind 
586 Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead 
587 a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) u0) 
588 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 
589 (Bind Abst) u0) (Bind Abst) u) t a4)))))) H4 t H7) in (let H10 \def (eq_ind T 
590 t0 (\lambda (t1: T).(arity g (CHead c0 (Bind Abst) u0) t1 a2)) H3 t H7) in 
591 (let H11 \def (eq_ind T u0 (\lambda (t1: T).((eq T t (THead (Bind Abst) u t)) 
592 \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
593 (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) t1) u (asucc 
594 g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind 
595 Abst) t1) (Bind Abst) u) t a4)))))) H9 u H8) in (let H12 \def (eq_ind T u0 
596 (\lambda (t1: T).(arity g (CHead c0 (Bind Abst) t1) t a2)) H10 u H8) in (let 
597 H13 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to 
598 (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A (asucc g a1) (AHead a3 
599 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) 
600 (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))))) 
601 H2 u H8) in (let H14 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 (asucc 
602 g a1))) H1 u H8) in (ex3_2_intro A A (\lambda (a3: A).(\lambda (a4: A).(eq A 
603 (AHead a1 a2) (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u 
604 (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind 
605 Abst) u) t a4))) a1 a2 (refl_equal A (AHead a1 a2)) H14 H12))))))))) 
606 H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda 
607 (_: (arity g c0 u0 a1)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to 
608 (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead a2 a3)))) 
609 (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) (\lambda (_: 
610 A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t a3))))))).(\lambda 
611 (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0 (AHead a1 a2))).(\lambda 
612 (_: (((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
613 A).(\lambda (a4: A).(eq A (AHead a1 a2) (AHead a3 a4)))) (\lambda (a3: 
614 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
615 (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))))))).(\lambda (H5: (eq T 
616 (THead (Flat Appl) u0 t0) (THead (Bind Abst) u t))).(let H6 \def (eq_ind T 
617 (THead (Flat Appl) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: 
618 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
619 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
620 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
621 Abst) u t) H5) in (False_ind (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq 
622 A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g 
623 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t 
624 a4)))) H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a0: 
625 A).(\lambda (_: (arity g c0 u0 (asucc g a0))).(\lambda (_: (((eq T u0 (THead 
626 (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A 
627 (asucc g a0) (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u 
628 (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind 
629 Abst) u) t a2))))))).(\lambda (t0: T).(\lambda (_: (arity g c0 t0 
630 a0)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
631 (a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda 
632 (_: A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity 
633 g (CHead c0 (Bind Abst) u) t a2))))))).(\lambda (H5: (eq T (THead (Flat Cast) 
634 u0 t0) (THead (Bind Abst) u t))).(let H6 \def (eq_ind T (THead (Flat Cast) u0 
635 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
636 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
637 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
638 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u t) 
639 H5) in (False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A a0 
640 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g 
641 a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t 
642 a2)))) H6))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: 
643 A).(\lambda (H1: (arity g c0 t0 a1)).(\lambda (H2: (((eq T t0 (THead (Bind 
644 Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead 
645 a2 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
646 (\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
647 a3))))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T 
648 t0 (THead (Bind Abst) u t))).(let H5 \def (f_equal T T (\lambda (e: T).e) t0 
649 (THead (Bind Abst) u t) H4) in (let H6 \def (eq_ind T t0 (\lambda (t1: 
650 T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
651 A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
652 A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
653 (CHead c0 (Bind Abst) u) t a4)))))) H2 (THead (Bind Abst) u t) H5) in (let H7 
654 \def (eq_ind T t0 (\lambda (t1: T).(arity g c0 t1 a1)) H1 (THead (Bind Abst) 
655 u t) H5) in (let H8 \def (H6 (refl_equal T (THead (Bind Abst) u t))) in 
656 (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) 
657 (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
658 A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) (ex3_2 A A 
659 (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: 
660 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
661 (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x0: A).(\lambda 
662 (x1: A).(\lambda (H9: (eq A a1 (AHead x0 x1))).(\lambda (H10: (arity g c0 u 
663 (asucc g x0))).(\lambda (H11: (arity g (CHead c0 (Bind Abst) u) t x1)).(let 
664 H12 \def (eq_ind A a1 (\lambda (a0: A).(leq g a0 a2)) H3 (AHead x0 x1) H9) in 
665 (let H13 \def (eq_ind A a1 (\lambda (a0: A).(arity g c0 (THead (Bind Abst) u 
666 t) a0)) H7 (AHead x0 x1) H9) in (let H_x \def (leq_gen_head g x0 x1 a2 H12) 
667 in (let H14 \def H_x in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq 
668 A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(leq g x0 a3))) 
669 (\lambda (_: A).(\lambda (a4: A).(leq g x1 a4))) (ex3_2 A A (\lambda (a3: 
670 A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
671 A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
672 (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x2: A).(\lambda (x3: A).(\lambda 
673 (H15: (eq A a2 (AHead x2 x3))).(\lambda (H16: (leq g x0 x2)).(\lambda (H17: 
674 (leq g x1 x3)).(eq_ind_r A (AHead x2 x3) (\lambda (a0: A).(ex3_2 A A (\lambda 
675 (a3: A).(\lambda (a4: A).(eq A a0 (AHead a3 a4)))) (\lambda (a3: A).(\lambda 
676 (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity 
677 g (CHead c0 (Bind Abst) u) t a4))))) (ex3_2_intro A A (\lambda (a3: 
678 A).(\lambda (a4: A).(eq A (AHead x2 x3) (AHead a3 a4)))) (\lambda (a3: 
679 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
680 (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) x2 x3 (refl_equal A (AHead 
681 x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) (asucc_repl g x0 x2 
682 H16)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H17)) a2 H15)))))) 
683 H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
684
685 theorem arity_gen_appl:
686  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a2: 
687 A).((arity g c (THead (Flat Appl) u t) a2) \to (ex2 A (\lambda (a1: A).(arity 
688 g c u a1)) (\lambda (a1: A).(arity g c t (AHead a1 a2)))))))))
689 \def
690  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a2: 
691 A).(\lambda (H: (arity g c (THead (Flat Appl) u t) a2)).(insert_eq T (THead 
692 (Flat Appl) u t) (\lambda (t0: T).(arity g c t0 a2)) (\lambda (_: T).(ex2 A 
693 (\lambda (a1: A).(arity g c u a1)) (\lambda (a1: A).(arity g c t (AHead a1 
694 a2))))) (\lambda (y: T).(\lambda (H0: (arity g c y a2)).(arity_ind g (\lambda 
695 (c0: C).(\lambda (t0: T).(\lambda (a: A).((eq T t0 (THead (Flat Appl) u t)) 
696 \to (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t 
697 (AHead a1 a)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T 
698 (TSort n) (THead (Flat Appl) u t))).(let H2 \def (eq_ind T (TSort n) (\lambda 
699 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
700 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
701 False])) I (THead (Flat Appl) u t) H1) in (False_ind (ex2 A (\lambda (a1: 
702 A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t (AHead a1 (ASort O 
703 n))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
704 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a: 
705 A).(\lambda (_: (arity g d u0 a)).(\lambda (_: (((eq T u0 (THead (Flat Appl) 
706 u t)) \to (ex2 A (\lambda (a1: A).(arity g d u a1)) (\lambda (a1: A).(arity g 
707 d t (AHead a1 a))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u 
708 t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
709 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
710 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u 
711 t) H4) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: 
712 A).(arity g c0 t (AHead a1 a)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
713 C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
714 Abst) u0))).(\lambda (a: A).(\lambda (_: (arity g d u0 (asucc g a))).(\lambda 
715 (_: (((eq T u0 (THead (Flat Appl) u t)) \to (ex2 A (\lambda (a1: A).(arity g 
716 d u a1)) (\lambda (a1: A).(arity g d t (AHead a1 (asucc g a)))))))).(\lambda 
717 (H4: (eq T (TLRef i) (THead (Flat Appl) u t))).(let H5 \def (eq_ind T (TLRef 
718 i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
719 _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
720 False])) I (THead (Flat Appl) u t) H4) in (False_ind (ex2 A (\lambda (a1: 
721 A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t (AHead a1 a)))) 
722 H5))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda (c0: 
723 C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u0 
724 a1)).(\lambda (_: (((eq T u0 (THead (Flat Appl) u t)) \to (ex2 A (\lambda 
725 (a3: A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 
726 a1))))))).(\lambda (t0: T).(\lambda (a0: A).(\lambda (_: (arity g (CHead c0 
727 (Bind b) u0) t0 a0)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t)) \to 
728 (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind b) u0) u a3)) (\lambda (a3: 
729 A).(arity g (CHead c0 (Bind b) u0) t (AHead a3 a0))))))).(\lambda (H6: (eq T 
730 (THead (Bind b) u0 t0) (THead (Flat Appl) u t))).(let H7 \def (eq_ind T 
731 (THead (Bind b) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: 
732 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
733 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
734 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
735 Appl) u t) H6) in (False_ind (ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
736 (\lambda (a3: A).(arity g c0 t (AHead a3 a0)))) H7)))))))))))))) (\lambda 
737 (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u0 (asucc 
738 g a1))).(\lambda (_: (((eq T u0 (THead (Flat Appl) u t)) \to (ex2 A (\lambda 
739 (a3: A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 (asucc g 
740 a1)))))))).(\lambda (t0: T).(\lambda (a0: A).(\lambda (_: (arity g (CHead c0 
741 (Bind Abst) u0) t0 a0)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t)) \to 
742 (ex2 A (\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u0) u a3)) (\lambda 
743 (a3: A).(arity g (CHead c0 (Bind Abst) u0) t (AHead a3 a0))))))).(\lambda 
744 (H5: (eq T (THead (Bind Abst) u0 t0) (THead (Flat Appl) u t))).(let H6 \def 
745 (eq_ind T (THead (Bind Abst) u0 t0) (\lambda (ee: T).(match ee in T return 
746 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
747 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
748 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
749 False])])) I (THead (Flat Appl) u t) H5) in (False_ind (ex2 A (\lambda (a3: 
750 A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 (AHead a1 
751 a0))))) H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: 
752 A).(\lambda (H1: (arity g c0 u0 a1)).(\lambda (H2: (((eq T u0 (THead (Flat 
753 Appl) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (a3: 
754 A).(arity g c0 t (AHead a3 a1))))))).(\lambda (t0: T).(\lambda (a0: 
755 A).(\lambda (H3: (arity g c0 t0 (AHead a1 a0))).(\lambda (H4: (((eq T t0 
756 (THead (Flat Appl) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
757 (\lambda (a3: A).(arity g c0 t (AHead a3 (AHead a1 a0)))))))).(\lambda (H5: 
758 (eq T (THead (Flat Appl) u0 t0) (THead (Flat Appl) u t))).(let H6 \def 
759 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
760 [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t1 _) 
761 \Rightarrow t1])) (THead (Flat Appl) u0 t0) (THead (Flat Appl) u t) H5) in 
762 ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: 
763 T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ 
764 t1) \Rightarrow t1])) (THead (Flat Appl) u0 t0) (THead (Flat Appl) u t) H5) 
765 in (\lambda (H8: (eq T u0 u)).(let H9 \def (eq_ind T t0 (\lambda (t1: T).((eq 
766 T t1 (THead (Flat Appl) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
767 (\lambda (a3: A).(arity g c0 t (AHead a3 (AHead a1 a0))))))) H4 t H7) in (let 
768 H10 \def (eq_ind T t0 (\lambda (t1: T).(arity g c0 t1 (AHead a1 a0))) H3 t 
769 H7) in (let H11 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead (Flat 
770 Appl) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (a3: 
771 A).(arity g c0 t (AHead a3 a1)))))) H2 u H8) in (let H12 \def (eq_ind T u0 
772 (\lambda (t1: T).(arity g c0 t1 a1)) H1 u H8) in (ex_intro2 A (\lambda (a3: 
773 A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 a0))) a1 H12 
774 H10))))))) H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a: 
775 A).(\lambda (_: (arity g c0 u0 (asucc g a))).(\lambda (_: (((eq T u0 (THead 
776 (Flat Appl) u t)) \to (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda 
777 (a1: A).(arity g c0 t (AHead a1 (asucc g a)))))))).(\lambda (t0: T).(\lambda 
778 (_: (arity g c0 t0 a)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t)) \to 
779 (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t 
780 (AHead a1 a))))))).(\lambda (H5: (eq T (THead (Flat Cast) u0 t0) (THead (Flat 
781 Appl) u t))).(let H6 \def (eq_ind T (THead (Flat Cast) u0 t0) (\lambda (ee: 
782 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
783 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K 
784 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) 
785 \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl \Rightarrow 
786 False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t) H5) in 
787 (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity 
788 g c0 t (AHead a1 a)))) H6))))))))))) (\lambda (c0: C).(\lambda (t0: 
789 T).(\lambda (a1: A).(\lambda (H1: (arity g c0 t0 a1)).(\lambda (H2: (((eq T 
790 t0 (THead (Flat Appl) u t)) \to (ex2 A (\lambda (a3: A).(arity g c0 u a3)) 
791 (\lambda (a3: A).(arity g c0 t (AHead a3 a1))))))).(\lambda (a0: A).(\lambda 
792 (H3: (leq g a1 a0)).(\lambda (H4: (eq T t0 (THead (Flat Appl) u t))).(let H5 
793 \def (f_equal T T (\lambda (e: T).e) t0 (THead (Flat Appl) u t) H4) in (let 
794 H6 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 (THead (Flat Appl) u t)) \to 
795 (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t 
796 (AHead a3 a1)))))) H2 (THead (Flat Appl) u t) H5) in (let H7 \def (eq_ind T 
797 t0 (\lambda (t1: T).(arity g c0 t1 a1)) H1 (THead (Flat Appl) u t) H5) in 
798 (let H8 \def (H6 (refl_equal T (THead (Flat Appl) u t))) in (ex2_ind A 
799 (\lambda (a3: A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 
800 a1))) (ex2 A (\lambda (a3: A).(arity g c0 u a3)) (\lambda (a3: A).(arity g c0 
801 t (AHead a3 a0)))) (\lambda (x: A).(\lambda (H9: (arity g c0 u x)).(\lambda 
802 (H10: (arity g c0 t (AHead x a1))).(ex_intro2 A (\lambda (a3: A).(arity g c0 
803 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 a0))) x H9 (arity_repl g c0 t 
804 (AHead x a1) H10 (AHead x a0) (leq_head g x x (leq_refl g x) a1 a0 H3)))))) 
805 H8))))))))))))) c y a2 H0))) H)))))).
806
807 theorem arity_gen_cast:
808  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a: 
809 A).((arity g c (THead (Flat Cast) u t) a) \to (land (arity g c u (asucc g a)) 
810 (arity g c t a)))))))
811 \def
812  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a: 
813 A).(\lambda (H: (arity g c (THead (Flat Cast) u t) a)).(insert_eq T (THead 
814 (Flat Cast) u t) (\lambda (t0: T).(arity g c t0 a)) (\lambda (_: T).(land 
815 (arity g c u (asucc g a)) (arity g c t a))) (\lambda (y: T).(\lambda (H0: 
816 (arity g c y a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: 
817 A).((eq T t0 (THead (Flat Cast) u t)) \to (land (arity g c0 u (asucc g a0)) 
818 (arity g c0 t a0)))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T 
819 (TSort n) (THead (Flat Cast) u t))).(let H2 \def (eq_ind T (TSort n) (\lambda 
820 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
821 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
822 False])) I (THead (Flat Cast) u t) H1) in (False_ind (land (arity g c0 u 
823 (asucc g (ASort O n))) (arity g c0 t (ASort O n))) H2))))) (\lambda (c0: 
824 C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
825 (CHead d (Bind Abbr) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 
826 a0)).(\lambda (_: (((eq T u0 (THead (Flat Cast) u t)) \to (land (arity g d u 
827 (asucc g a0)) (arity g d t a0))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat 
828 Cast) u t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T 
829 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
830 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) u 
831 t) H4) in (False_ind (land (arity g c0 u (asucc g a0)) (arity g c0 t a0)) 
832 H5))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
833 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abst) u0))).(\lambda (a0: 
834 A).(\lambda (_: (arity g d u0 (asucc g a0))).(\lambda (_: (((eq T u0 (THead 
835 (Flat Cast) u t)) \to (land (arity g d u (asucc g (asucc g a0))) (arity g d t 
836 (asucc g a0)))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) u 
837 t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
838 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
839 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) u 
840 t) H4) in (False_ind (land (arity g c0 u (asucc g a0)) (arity g c0 t a0)) 
841 H5))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda (c0: 
842 C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u0 
843 a1)).(\lambda (_: (((eq T u0 (THead (Flat Cast) u t)) \to (land (arity g c0 u 
844 (asucc g a1)) (arity g c0 t a1))))).(\lambda (t0: T).(\lambda (a2: 
845 A).(\lambda (_: (arity g (CHead c0 (Bind b) u0) t0 a2)).(\lambda (_: (((eq T 
846 t0 (THead (Flat Cast) u t)) \to (land (arity g (CHead c0 (Bind b) u0) u 
847 (asucc g a2)) (arity g (CHead c0 (Bind b) u0) t a2))))).(\lambda (H6: (eq T 
848 (THead (Bind b) u0 t0) (THead (Flat Cast) u t))).(let H7 \def (eq_ind T 
849 (THead (Bind b) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: 
850 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
851 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
852 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
853 Cast) u t) H6) in (False_ind (land (arity g c0 u (asucc g a2)) (arity g c0 t 
854 a2)) H7)))))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: 
855 A).(\lambda (_: (arity g c0 u0 (asucc g a1))).(\lambda (_: (((eq T u0 (THead 
856 (Flat Cast) u t)) \to (land (arity g c0 u (asucc g (asucc g a1))) (arity g c0 
857 t (asucc g a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g 
858 (CHead c0 (Bind Abst) u0) t0 a2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) 
859 u t)) \to (land (arity g (CHead c0 (Bind Abst) u0) u (asucc g a2)) (arity g 
860 (CHead c0 (Bind Abst) u0) t a2))))).(\lambda (H5: (eq T (THead (Bind Abst) u0 
861 t0) (THead (Flat Cast) u t))).(let H6 \def (eq_ind T (THead (Bind Abst) u0 
862 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
863 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
864 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
865 \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Cast) u t) 
866 H5) in (False_ind (land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t 
867 (AHead a1 a2))) H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda 
868 (a1: A).(\lambda (_: (arity g c0 u0 a1)).(\lambda (_: (((eq T u0 (THead (Flat 
869 Cast) u t)) \to (land (arity g c0 u (asucc g a1)) (arity g c0 t 
870 a1))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0 (AHead 
871 a1 a2))).(\lambda (_: (((eq T t0 (THead (Flat Cast) u t)) \to (land (arity g 
872 c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2)))))).(\lambda (H5: 
873 (eq T (THead (Flat Appl) u0 t0) (THead (Flat Cast) u t))).(let H6 \def 
874 (eq_ind T (THead (Flat Appl) u0 t0) (\lambda (ee: T).(match ee in T return 
875 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
876 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
877 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f 
878 in F return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast 
879 \Rightarrow False])])])) I (THead (Flat Cast) u t) H5) in (False_ind (land 
880 (arity g c0 u (asucc g a2)) (arity g c0 t a2)) H6)))))))))))) (\lambda (c0: 
881 C).(\lambda (u0: T).(\lambda (a0: A).(\lambda (H1: (arity g c0 u0 (asucc g 
882 a0))).(\lambda (H2: (((eq T u0 (THead (Flat Cast) u t)) \to (land (arity g c0 
883 u (asucc g (asucc g a0))) (arity g c0 t (asucc g a0)))))).(\lambda (t0: 
884 T).(\lambda (H3: (arity g c0 t0 a0)).(\lambda (H4: (((eq T t0 (THead (Flat 
885 Cast) u t)) \to (land (arity g c0 u (asucc g a0)) (arity g c0 t 
886 a0))))).(\lambda (H5: (eq T (THead (Flat Cast) u0 t0) (THead (Flat Cast) u 
887 t))).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda 
888 (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead 
889 _ t1 _) \Rightarrow t1])) (THead (Flat Cast) u0 t0) (THead (Flat Cast) u t) 
890 H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return 
891 (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 
892 | (THead _ _ t1) \Rightarrow t1])) (THead (Flat Cast) u0 t0) (THead (Flat 
893 Cast) u t) H5) in (\lambda (H8: (eq T u0 u)).(let H9 \def (eq_ind T t0 
894 (\lambda (t1: T).((eq T t1 (THead (Flat Cast) u t)) \to (land (arity g c0 u 
895 (asucc g a0)) (arity g c0 t a0)))) H4 t H7) in (let H10 \def (eq_ind T t0 
896 (\lambda (t1: T).(arity g c0 t1 a0)) H3 t H7) in (let H11 \def (eq_ind T u0 
897 (\lambda (t1: T).((eq T t1 (THead (Flat Cast) u t)) \to (land (arity g c0 u 
898 (asucc g (asucc g a0))) (arity g c0 t (asucc g a0))))) H2 u H8) in (let H12 
899 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 (asucc g a0))) H1 u H8) in 
900 (conj (arity g c0 u (asucc g a0)) (arity g c0 t a0) H12 H10))))))) 
901 H6))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda 
902 (H1: (arity g c0 t0 a1)).(\lambda (H2: (((eq T t0 (THead (Flat Cast) u t)) 
903 \to (land (arity g c0 u (asucc g a1)) (arity g c0 t a1))))).(\lambda (a2: 
904 A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T t0 (THead (Flat Cast) u 
905 t))).(let H5 \def (f_equal T T (\lambda (e: T).e) t0 (THead (Flat Cast) u t) 
906 H4) in (let H6 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 (THead (Flat 
907 Cast) u t)) \to (land (arity g c0 u (asucc g a1)) (arity g c0 t a1)))) H2 
908 (THead (Flat Cast) u t) H5) in (let H7 \def (eq_ind T t0 (\lambda (t1: 
909 T).(arity g c0 t1 a1)) H1 (THead (Flat Cast) u t) H5) in (let H8 \def (H6 
910 (refl_equal T (THead (Flat Cast) u t))) in (and_ind (arity g c0 u (asucc g 
911 a1)) (arity g c0 t a1) (land (arity g c0 u (asucc g a2)) (arity g c0 t a2)) 
912 (\lambda (H9: (arity g c0 u (asucc g a1))).(\lambda (H10: (arity g c0 t 
913 a1)).(conj (arity g c0 u (asucc g a2)) (arity g c0 t a2) (arity_repl g c0 u 
914 (asucc g a1) H9 (asucc g a2) (asucc_repl g a1 a2 H3)) (arity_repl g c0 t a1 
915 H10 a2 H3)))) H8))))))))))))) c y a H0))) H)))))).
916
917 theorem arity_gen_appls:
918  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (vs: TList).(\forall 
919 (a2: A).((arity g c (THeads (Flat Appl) vs t) a2) \to (ex A (\lambda (a: 
920 A).(arity g c t a))))))))
921 \def
922  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (vs: 
923 TList).(TList_ind (\lambda (t0: TList).(\forall (a2: A).((arity g c (THeads 
924 (Flat Appl) t0 t) a2) \to (ex A (\lambda (a: A).(arity g c t a)))))) (\lambda 
925 (a2: A).(\lambda (H: (arity g c t a2)).(ex_intro A (\lambda (a: A).(arity g c 
926 t a)) a2 H))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: ((\forall 
927 (a2: A).((arity g c (THeads (Flat Appl) t1 t) a2) \to (ex A (\lambda (a: 
928 A).(arity g c t a))))))).(\lambda (a2: A).(\lambda (H0: (arity g c (THead 
929 (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a2)).(let H1 \def (arity_gen_appl g 
930 c t0 (THeads (Flat Appl) t1 t) a2 H0) in (ex2_ind A (\lambda (a1: A).(arity g 
931 c t0 a1)) (\lambda (a1: A).(arity g c (THeads (Flat Appl) t1 t) (AHead a1 
932 a2))) (ex A (\lambda (a: A).(arity g c t a))) (\lambda (x: A).(\lambda (_: 
933 (arity g c t0 x)).(\lambda (H3: (arity g c (THeads (Flat Appl) t1 t) (AHead x 
934 a2))).(let H_x \def (H (AHead x a2) H3) in (let H4 \def H_x in (ex_ind A 
935 (\lambda (a: A).(arity g c t a)) (ex A (\lambda (a: A).(arity g c t a))) 
936 (\lambda (x0: A).(\lambda (H5: (arity g c t x0)).(ex_intro A (\lambda (a: 
937 A).(arity g c t a)) x0 H5))) H4)))))) H1))))))) vs)))).
938
939 theorem arity_gen_lift:
940  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).(\forall (h: 
941 nat).(\forall (d: nat).((arity g c1 (lift h d t) a) \to (\forall (c2: 
942 C).((drop h d c1 c2) \to (arity g c2 t a)))))))))
943 \def
944  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (h: 
945 nat).(\lambda (d: nat).(\lambda (H: (arity g c1 (lift h d t) a)).(insert_eq T 
946 (lift h d t) (\lambda (t0: T).(arity g c1 t0 a)) (\lambda (_: T).(\forall 
947 (c2: C).((drop h d c1 c2) \to (arity g c2 t a)))) (\lambda (y: T).(\lambda 
948 (H0: (arity g c1 y a)).(unintro T t (\lambda (t0: T).((eq T y (lift h d t0)) 
949 \to (\forall (c2: C).((drop h d c1 c2) \to (arity g c2 t0 a))))) (unintro nat 
950 d (\lambda (n: nat).(\forall (x: T).((eq T y (lift h n x)) \to (\forall (c2: 
951 C).((drop h n c1 c2) \to (arity g c2 x a)))))) (arity_ind g (\lambda (c: 
952 C).(\lambda (t0: T).(\lambda (a0: A).(\forall (x: nat).(\forall (x0: T).((eq 
953 T t0 (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to (arity g c2 x0 
954 a0))))))))) (\lambda (c: C).(\lambda (n: nat).(\lambda (x: nat).(\lambda (x0: 
955 T).(\lambda (H1: (eq T (TSort n) (lift h x x0))).(\lambda (c2: C).(\lambda 
956 (_: (drop h x c c2)).(eq_ind_r T (TSort n) (\lambda (t0: T).(arity g c2 t0 
957 (ASort O n))) (arity_sort g c2 n) x0 (lift_gen_sort h x n x0 H1))))))))) 
958 (\lambda (c: C).(\lambda (d0: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
959 (H1: (getl i c (CHead d0 (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H2: 
960 (arity g d0 u a0)).(\lambda (H3: ((\forall (x: nat).(\forall (x0: T).((eq T u 
961 (lift h x x0)) \to (\forall (c2: C).((drop h x d0 c2) \to (arity g c2 x0 
962 a0)))))))).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T (TLRef i) 
963 (lift h x x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(let H_x \def 
964 (lift_gen_lref x0 x h i H4) in (let H6 \def H_x in (or_ind (land (lt i x) (eq 
965 T x0 (TLRef i))) (land (le (plus x h) i) (eq T x0 (TLRef (minus i h)))) 
966 (arity g c2 x0 a0) (\lambda (H7: (land (lt i x) (eq T x0 (TLRef 
967 i)))).(and_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8: 
968 (lt i x)).(\lambda (H9: (eq T x0 (TLRef i))).(eq_ind_r T (TLRef i) (\lambda 
969 (t0: T).(arity g c2 t0 a0)) (let H10 \def (eq_ind nat x (\lambda (n: 
970 nat).(drop h n c c2)) H5 (S (plus i (minus x (S i)))) (lt_plus_minus i x H8)) 
971 in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus x (S 
972 i)) v)))) (\lambda (v: T).(\lambda (e0: C).(getl i c2 (CHead e0 (Bind Abbr) 
973 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (minus x (S i)) d0 e0))) 
974 (arity g c2 (TLRef i) a0) (\lambda (x1: T).(\lambda (x2: C).(\lambda (H11: 
975 (eq T u (lift h (minus x (S i)) x1))).(\lambda (H12: (getl i c2 (CHead x2 
976 (Bind Abbr) x1))).(\lambda (H13: (drop h (minus x (S i)) d0 x2)).(let H14 
977 \def (eq_ind T u (\lambda (t0: T).(\forall (x3: nat).(\forall (x4: T).((eq T 
978 t0 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 d0 c3) \to (arity g c3 x4 
979 a0))))))) H3 (lift h (minus x (S i)) x1) H11) in (let H15 \def (eq_ind T u 
980 (\lambda (t0: T).(arity g d0 t0 a0)) H2 (lift h (minus x (S i)) x1) H11) in 
981 (arity_abbr g c2 x2 x1 i H12 a0 (H14 (minus x (S i)) x1 (refl_equal T (lift h 
982 (minus x (S i)) x1)) x2 H13))))))))) (getl_drop_conf_lt Abbr c d0 u i H1 c2 h 
983 (minus x (S i)) H10))) x0 H9))) H7)) (\lambda (H7: (land (le (plus x h) i) 
984 (eq T x0 (TLRef (minus i h))))).(and_ind (le (plus x h) i) (eq T x0 (TLRef 
985 (minus i h))) (arity g c2 x0 a0) (\lambda (H8: (le (plus x h) i)).(\lambda 
986 (H9: (eq T x0 (TLRef (minus i h)))).(eq_ind_r T (TLRef (minus i h)) (\lambda 
987 (t0: T).(arity g c2 t0 a0)) (arity_abbr g c2 d0 u (minus i h) 
988 (getl_drop_conf_ge i (CHead d0 (Bind Abbr) u) c H1 c2 h x H5 H8) a0 H2) x0 
989 H9))) H7)) H6)))))))))))))))) (\lambda (c: C).(\lambda (d0: C).(\lambda (u: 
990 T).(\lambda (i: nat).(\lambda (H1: (getl i c (CHead d0 (Bind Abst) 
991 u))).(\lambda (a0: A).(\lambda (H2: (arity g d0 u (asucc g a0))).(\lambda 
992 (H3: ((\forall (x: nat).(\forall (x0: T).((eq T u (lift h x x0)) \to (\forall 
993 (c2: C).((drop h x d0 c2) \to (arity g c2 x0 (asucc g a0))))))))).(\lambda 
994 (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T (TLRef i) (lift h x 
995 x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(let H_x \def 
996 (lift_gen_lref x0 x h i H4) in (let H6 \def H_x in (or_ind (land (lt i x) (eq 
997 T x0 (TLRef i))) (land (le (plus x h) i) (eq T x0 (TLRef (minus i h)))) 
998 (arity g c2 x0 a0) (\lambda (H7: (land (lt i x) (eq T x0 (TLRef 
999 i)))).(and_ind (lt i x) (eq T x0 (TLRef i)) (arity g c2 x0 a0) (\lambda (H8: 
1000 (lt i x)).(\lambda (H9: (eq T x0 (TLRef i))).(eq_ind_r T (TLRef i) (\lambda 
1001 (t0: T).(arity g c2 t0 a0)) (let H10 \def (eq_ind nat x (\lambda (n: 
1002 nat).(drop h n c c2)) H5 (S (plus i (minus x (S i)))) (lt_plus_minus i x H8)) 
1003 in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus x (S 
1004 i)) v)))) (\lambda (v: T).(\lambda (e0: C).(getl i c2 (CHead e0 (Bind Abst) 
1005 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (minus x (S i)) d0 e0))) 
1006 (arity g c2 (TLRef i) a0) (\lambda (x1: T).(\lambda (x2: C).(\lambda (H11: 
1007 (eq T u (lift h (minus x (S i)) x1))).(\lambda (H12: (getl i c2 (CHead x2 
1008 (Bind Abst) x1))).(\lambda (H13: (drop h (minus x (S i)) d0 x2)).(let H14 
1009 \def (eq_ind T u (\lambda (t0: T).(\forall (x3: nat).(\forall (x4: T).((eq T 
1010 t0 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 d0 c3) \to (arity g c3 x4 
1011 (asucc g a0)))))))) H3 (lift h (minus x (S i)) x1) H11) in (let H15 \def 
1012 (eq_ind T u (\lambda (t0: T).(arity g d0 t0 (asucc g a0))) H2 (lift h (minus 
1013 x (S i)) x1) H11) in (arity_abst g c2 x2 x1 i H12 a0 (H14 (minus x (S i)) x1 
1014 (refl_equal T (lift h (minus x (S i)) x1)) x2 H13))))))))) (getl_drop_conf_lt 
1015 Abst c d0 u i H1 c2 h (minus x (S i)) H10))) x0 H9))) H7)) (\lambda (H7: 
1016 (land (le (plus x h) i) (eq T x0 (TLRef (minus i h))))).(and_ind (le (plus x 
1017 h) i) (eq T x0 (TLRef (minus i h))) (arity g c2 x0 a0) (\lambda (H8: (le 
1018 (plus x h) i)).(\lambda (H9: (eq T x0 (TLRef (minus i h)))).(eq_ind_r T 
1019 (TLRef (minus i h)) (\lambda (t0: T).(arity g c2 t0 a0)) (arity_abst g c2 d0 
1020 u (minus i h) (getl_drop_conf_ge i (CHead d0 (Bind Abst) u) c H1 c2 h x H5 
1021 H8) a0 H2) x0 H9))) H7)) H6)))))))))))))))) (\lambda (b: B).(\lambda (H1: 
1022 (not (eq B b Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: 
1023 A).(\lambda (H2: (arity g c u a1)).(\lambda (H3: ((\forall (x: nat).(\forall 
1024 (x0: T).((eq T u (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to 
1025 (arity g c2 x0 a1)))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H4: 
1026 (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H5: ((\forall (x: 
1027 nat).(\forall (x0: T).((eq T t0 (lift h x x0)) \to (\forall (c2: C).((drop h 
1028 x (CHead c (Bind b) u) c2) \to (arity g c2 x0 a2)))))))).(\lambda (x: 
1029 nat).(\lambda (x0: T).(\lambda (H6: (eq T (THead (Bind b) u t0) (lift h x 
1030 x0))).(\lambda (c2: C).(\lambda (H7: (drop h x c c2)).(ex3_2_ind T T (\lambda 
1031 (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind b) y0 z)))) (\lambda (y0: 
1032 T).(\lambda (_: T).(eq T u (lift h x y0)))) (\lambda (_: T).(\lambda (z: 
1033 T).(eq T t0 (lift h (S x) z)))) (arity g c2 x0 a2) (\lambda (x1: T).(\lambda 
1034 (x2: T).(\lambda (H8: (eq T x0 (THead (Bind b) x1 x2))).(\lambda (H9: (eq T u 
1035 (lift h x x1))).(\lambda (H10: (eq T t0 (lift h (S x) x2))).(eq_ind_r T 
1036 (THead (Bind b) x1 x2) (\lambda (t1: T).(arity g c2 t1 a2)) (let H11 \def 
1037 (eq_ind T t0 (\lambda (t1: T).(\forall (x3: nat).(\forall (x4: T).((eq T t1 
1038 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 (CHead c (Bind b) u) c3) \to 
1039 (arity g c3 x4 a2))))))) H5 (lift h (S x) x2) H10) in (let H12 \def (eq_ind T 
1040 t0 (\lambda (t1: T).(arity g (CHead c (Bind b) u) t1 a2)) H4 (lift h (S x) 
1041 x2) H10) in (let H13 \def (eq_ind T u (\lambda (t1: T).(arity g (CHead c 
1042 (Bind b) t1) (lift h (S x) x2) a2)) H12 (lift h x x1) H9) in (let H14 \def 
1043 (eq_ind T u (\lambda (t1: T).(\forall (x3: nat).(\forall (x4: T).((eq T (lift 
1044 h (S x) x2) (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 (CHead c (Bind 
1045 b) t1) c3) \to (arity g c3 x4 a2))))))) H11 (lift h x x1) H9) in (let H15 
1046 \def (eq_ind T u (\lambda (t1: T).(\forall (x3: nat).(\forall (x4: T).((eq T 
1047 t1 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 c c3) \to (arity g c3 x4 
1048 a1))))))) H3 (lift h x x1) H9) in (let H16 \def (eq_ind T u (\lambda (t1: 
1049 T).(arity g c t1 a1)) H2 (lift h x x1) H9) in (arity_bind g b H1 c2 x1 a1 
1050 (H15 x x1 (refl_equal T (lift h x x1)) c2 H7) x2 a2 (H14 (S x) x2 (refl_equal 
1051 T (lift h (S x) x2)) (CHead c2 (Bind b) x1) (drop_skip_bind h x c c2 H7 b 
1052 x1))))))))) x0 H8)))))) (lift_gen_bind b u t0 x0 h x H6)))))))))))))))))) 
1053 (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H1: (arity g c u 
1054 (asucc g a1))).(\lambda (H2: ((\forall (x: nat).(\forall (x0: T).((eq T u 
1055 (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to (arity g c2 x0 
1056 (asucc g a1))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H3: (arity g 
1057 (CHead c (Bind Abst) u) t0 a2)).(\lambda (H4: ((\forall (x: nat).(\forall 
1058 (x0: T).((eq T t0 (lift h x x0)) \to (\forall (c2: C).((drop h x (CHead c 
1059 (Bind Abst) u) c2) \to (arity g c2 x0 a2)))))))).(\lambda (x: nat).(\lambda 
1060 (x0: T).(\lambda (H5: (eq T (THead (Bind Abst) u t0) (lift h x x0))).(\lambda 
1061 (c2: C).(\lambda (H6: (drop h x c c2)).(ex3_2_ind T T (\lambda (y0: 
1062 T).(\lambda (z: T).(eq T x0 (THead (Bind Abst) y0 z)))) (\lambda (y0: 
1063 T).(\lambda (_: T).(eq T u (lift h x y0)))) (\lambda (_: T).(\lambda (z: 
1064 T).(eq T t0 (lift h (S x) z)))) (arity g c2 x0 (AHead a1 a2)) (\lambda (x1: 
1065 T).(\lambda (x2: T).(\lambda (H7: (eq T x0 (THead (Bind Abst) x1 
1066 x2))).(\lambda (H8: (eq T u (lift h x x1))).(\lambda (H9: (eq T t0 (lift h (S 
1067 x) x2))).(eq_ind_r T (THead (Bind Abst) x1 x2) (\lambda (t1: T).(arity g c2 
1068 t1 (AHead a1 a2))) (let H10 \def (eq_ind T t0 (\lambda (t1: T).(\forall (x3: 
1069 nat).(\forall (x4: T).((eq T t1 (lift h x3 x4)) \to (\forall (c3: C).((drop h 
1070 x3 (CHead c (Bind Abst) u) c3) \to (arity g c3 x4 a2))))))) H4 (lift h (S x) 
1071 x2) H9) in (let H11 \def (eq_ind T t0 (\lambda (t1: T).(arity g (CHead c 
1072 (Bind Abst) u) t1 a2)) H3 (lift h (S x) x2) H9) in (let H12 \def (eq_ind T u 
1073 (\lambda (t1: T).(arity g (CHead c (Bind Abst) t1) (lift h (S x) x2) a2)) H11 
1074 (lift h x x1) H8) in (let H13 \def (eq_ind T u (\lambda (t1: T).(\forall (x3: 
1075 nat).(\forall (x4: T).((eq T (lift h (S x) x2) (lift h x3 x4)) \to (\forall 
1076 (c3: C).((drop h x3 (CHead c (Bind Abst) t1) c3) \to (arity g c3 x4 a2))))))) 
1077 H10 (lift h x x1) H8) in (let H14 \def (eq_ind T u (\lambda (t1: T).(\forall 
1078 (x3: nat).(\forall (x4: T).((eq T t1 (lift h x3 x4)) \to (\forall (c3: 
1079 C).((drop h x3 c c3) \to (arity g c3 x4 (asucc g a1)))))))) H2 (lift h x x1) 
1080 H8) in (let H15 \def (eq_ind T u (\lambda (t1: T).(arity g c t1 (asucc g 
1081 a1))) H1 (lift h x x1) H8) in (arity_head g c2 x1 a1 (H14 x x1 (refl_equal T 
1082 (lift h x x1)) c2 H6) x2 a2 (H13 (S x) x2 (refl_equal T (lift h (S x) x2)) 
1083 (CHead c2 (Bind Abst) x1) (drop_skip_bind h x c c2 H6 Abst x1))))))))) x0 
1084 H7)))))) (lift_gen_bind Abst u t0 x0 h x H5)))))))))))))))) (\lambda (c: 
1085 C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H1: (arity g c u a1)).(\lambda 
1086 (H2: ((\forall (x: nat).(\forall (x0: T).((eq T u (lift h x x0)) \to (\forall 
1087 (c2: C).((drop h x c c2) \to (arity g c2 x0 a1)))))))).(\lambda (t0: 
1088 T).(\lambda (a2: A).(\lambda (H3: (arity g c t0 (AHead a1 a2))).(\lambda (H4: 
1089 ((\forall (x: nat).(\forall (x0: T).((eq T t0 (lift h x x0)) \to (\forall 
1090 (c2: C).((drop h x c c2) \to (arity g c2 x0 (AHead a1 a2))))))))).(\lambda 
1091 (x: nat).(\lambda (x0: T).(\lambda (H5: (eq T (THead (Flat Appl) u t0) (lift 
1092 h x x0))).(\lambda (c2: C).(\lambda (H6: (drop h x c c2)).(ex3_2_ind T T 
1093 (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Appl) y0 z)))) 
1094 (\lambda (y0: T).(\lambda (_: T).(eq T u (lift h x y0)))) (\lambda (_: 
1095 T).(\lambda (z: T).(eq T t0 (lift h x z)))) (arity g c2 x0 a2) (\lambda (x1: 
1096 T).(\lambda (x2: T).(\lambda (H7: (eq T x0 (THead (Flat Appl) x1 
1097 x2))).(\lambda (H8: (eq T u (lift h x x1))).(\lambda (H9: (eq T t0 (lift h x 
1098 x2))).(eq_ind_r T (THead (Flat Appl) x1 x2) (\lambda (t1: T).(arity g c2 t1 
1099 a2)) (let H10 \def (eq_ind T t0 (\lambda (t1: T).(\forall (x3: nat).(\forall 
1100 (x4: T).((eq T t1 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 c c3) \to 
1101 (arity g c3 x4 (AHead a1 a2)))))))) H4 (lift h x x2) H9) in (let H11 \def 
1102 (eq_ind T t0 (\lambda (t1: T).(arity g c t1 (AHead a1 a2))) H3 (lift h x x2) 
1103 H9) in (let H12 \def (eq_ind T u (\lambda (t1: T).(\forall (x3: nat).(\forall 
1104 (x4: T).((eq T t1 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 c c3) \to 
1105 (arity g c3 x4 a1))))))) H2 (lift h x x1) H8) in (let H13 \def (eq_ind T u 
1106 (\lambda (t1: T).(arity g c t1 a1)) H1 (lift h x x1) H8) in (arity_appl g c2 
1107 x1 a1 (H12 x x1 (refl_equal T (lift h x x1)) c2 H6) x2 a2 (H10 x x2 
1108 (refl_equal T (lift h x x2)) c2 H6)))))) x0 H7)))))) (lift_gen_flat Appl u t0 
1109 x0 h x H5)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a0: 
1110 A).(\lambda (H1: (arity g c u (asucc g a0))).(\lambda (H2: ((\forall (x: 
1111 nat).(\forall (x0: T).((eq T u (lift h x x0)) \to (\forall (c2: C).((drop h x 
1112 c c2) \to (arity g c2 x0 (asucc g a0))))))))).(\lambda (t0: T).(\lambda (H3: 
1113 (arity g c t0 a0)).(\lambda (H4: ((\forall (x: nat).(\forall (x0: T).((eq T 
1114 t0 (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to (arity g c2 x0 
1115 a0)))))))).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H5: (eq T (THead 
1116 (Flat Cast) u t0) (lift h x x0))).(\lambda (c2: C).(\lambda (H6: (drop h x c 
1117 c2)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat 
1118 Cast) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u (lift h x y0)))) 
1119 (\lambda (_: T).(\lambda (z: T).(eq T t0 (lift h x z)))) (arity g c2 x0 a0) 
1120 (\lambda (x1: T).(\lambda (x2: T).(\lambda (H7: (eq T x0 (THead (Flat Cast) 
1121 x1 x2))).(\lambda (H8: (eq T u (lift h x x1))).(\lambda (H9: (eq T t0 (lift h 
1122 x x2))).(eq_ind_r T (THead (Flat Cast) x1 x2) (\lambda (t1: T).(arity g c2 t1 
1123 a0)) (let H10 \def (eq_ind T t0 (\lambda (t1: T).(\forall (x3: nat).(\forall 
1124 (x4: T).((eq T t1 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 c c3) \to 
1125 (arity g c3 x4 a0))))))) H4 (lift h x x2) H9) in (let H11 \def (eq_ind T t0 
1126 (\lambda (t1: T).(arity g c t1 a0)) H3 (lift h x x2) H9) in (let H12 \def 
1127 (eq_ind T u (\lambda (t1: T).(\forall (x3: nat).(\forall (x4: T).((eq T t1 
1128 (lift h x3 x4)) \to (\forall (c3: C).((drop h x3 c c3) \to (arity g c3 x4 
1129 (asucc g a0)))))))) H2 (lift h x x1) H8) in (let H13 \def (eq_ind T u 
1130 (\lambda (t1: T).(arity g c t1 (asucc g a0))) H1 (lift h x x1) H8) in 
1131 (arity_cast g c2 x1 a0 (H12 x x1 (refl_equal T (lift h x x1)) c2 H6) x2 (H10 
1132 x x2 (refl_equal T (lift h x x2)) c2 H6)))))) x0 H7)))))) (lift_gen_flat Cast 
1133 u t0 x0 h x H5))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: 
1134 A).(\lambda (_: (arity g c t0 a1)).(\lambda (H2: ((\forall (x: nat).(\forall 
1135 (x0: T).((eq T t0 (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to 
1136 (arity g c2 x0 a1)))))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 
1137 a2)).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T t0 (lift h x 
1138 x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(arity_repl g c2 x0 a1 
1139 (H2 x x0 H4 c2 H5) a2 H3))))))))))))) c1 y a H0))))) H))))))).
1140