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