]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1A/arity/pr3.ma
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / arity / pr3.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_1A/csuba/arity.ma".
18
19 include "basic_1A/pr3/fwd.ma".
20
21 include "basic_1A/pr1/fwd.ma".
22
23 include "basic_1A/wcpr0/getl.ma".
24
25 include "basic_1A/pr0/props.ma".
26
27 include "basic_1A/arity/subst0.ma".
28
29 lemma arity_sred_wcpr0_pr0:
30  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g 
31 c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1 
32 t2) \to (arity g c2 t2 a)))))))))
33 \def
34  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (a: A).(\lambda 
35 (H: (arity g c1 t1 a)).(arity_ind g (\lambda (c: C).(\lambda (t: T).(\lambda 
36 (a0: A).(\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to 
37 (arity g c2 t2 a0)))))))) (\lambda (c: C).(\lambda (n: nat).(\lambda (c2: 
38 C).(\lambda (_: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H1: (pr0 (TSort n) 
39 t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(arity g c2 t (ASort O n))) 
40 (arity_sort g c2 n) t2 (pr0_gen_sort t2 n H1)))))))) (\lambda (c: C).(\lambda 
41 (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d 
42 (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity g d u a0)).(\lambda 
43 (H2: ((\forall (c2: C).((wcpr0 d c2) \to (\forall (t2: T).((pr0 u t2) \to 
44 (arity g c2 t2 a0))))))).(\lambda (c2: C).(\lambda (H3: (wcpr0 c 
45 c2)).(\lambda (t2: T).(\lambda (H4: (pr0 (TLRef i) t2)).(eq_ind_r T (TLRef i) 
46 (\lambda (t: T).(arity g c2 t a0)) (ex3_2_ind C T (\lambda (e2: C).(\lambda 
47 (u2: T).(getl i c2 (CHead e2 (Bind Abbr) u2)))) (\lambda (e2: C).(\lambda (_: 
48 T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u u2))) (arity g c2 
49 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (getl i c2 
50 (CHead x0 (Bind Abbr) x1))).(\lambda (H6: (wcpr0 d x0)).(\lambda (H7: (pr0 u 
51 x1)).(arity_abbr g c2 x0 x1 i H5 a0 (H2 x0 H6 x1 H7))))))) (wcpr0_getl c c2 
52 H3 i d u (Bind Abbr) H0)) t2 (pr0_gen_lref t2 i H4)))))))))))))) (\lambda (c: 
53 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c 
54 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity g d u (asucc g 
55 a0))).(\lambda (H2: ((\forall (c2: C).((wcpr0 d c2) \to (\forall (t2: 
56 T).((pr0 u t2) \to (arity g c2 t2 (asucc g a0)))))))).(\lambda (c2: 
57 C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H4: (pr0 (TLRef i) 
58 t2)).(eq_ind_r T (TLRef i) (\lambda (t: T).(arity g c2 t a0)) (ex3_2_ind C T 
59 (\lambda (e2: C).(\lambda (u2: T).(getl i c2 (CHead e2 (Bind Abst) u2)))) 
60 (\lambda (e2: C).(\lambda (_: T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2: 
61 T).(pr0 u u2))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: 
62 T).(\lambda (H5: (getl i c2 (CHead x0 (Bind Abst) x1))).(\lambda (H6: (wcpr0 
63 d x0)).(\lambda (H7: (pr0 u x1)).(arity_abst g c2 x0 x1 i H5 a0 (H2 x0 H6 x1 
64 H7))))))) (wcpr0_getl c c2 H3 i d u (Bind Abst) H0)) t2 (pr0_gen_lref t2 i 
65 H4)))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda 
66 (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u 
67 a1)).(\lambda (H2: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 
68 u t2) \to (arity g c2 t2 a1))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda 
69 (H3: (arity g (CHead c (Bind b) u) t a2)).(\lambda (H4: ((\forall (c2: 
70 C).((wcpr0 (CHead c (Bind b) u) c2) \to (\forall (t2: T).((pr0 t t2) \to 
71 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H5: (wcpr0 c 
72 c2)).(\lambda (t2: T).(\lambda (H6: (pr0 (THead (Bind b) u t) t2)).(insert_eq 
73 T (THead (Bind b) u t) (\lambda (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g 
74 c2 t2 a2)) (\lambda (y: T).(\lambda (H7: (pr0 y t2)).(pr0_ind (\lambda (t0: 
75 T).(\lambda (t3: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 t3 a2)))) 
76 (\lambda (t0: T).(\lambda (H8: (eq T t0 (THead (Bind b) u t))).(let H9 \def 
77 (f_equal T T (\lambda (e: T).e) t0 (THead (Bind b) u t) H8) in (eq_ind_r T 
78 (THead (Bind b) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_bind g b H0 
79 c2 u a1 (H2 c2 H5 u (pr0_refl u)) t a2 (H4 (CHead c2 (Bind b) u) (wcpr0_comp 
80 c c2 H5 u u (pr0_refl u) (Bind b)) t (pr0_refl t))) t0 H9)))) (\lambda (u1: 
81 T).(\lambda (u2: T).(\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (((eq T u1 
82 (THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda 
83 (t4: T).(\lambda (H10: (pr0 t3 t4)).(\lambda (H11: (((eq T t3 (THead (Bind b) 
84 u t)) \to (arity g c2 t4 a2)))).(\lambda (k: K).(\lambda (H12: (eq T (THead k 
85 u1 t3) (THead (Bind b) u t))).(let H13 \def (f_equal T K (\lambda (e: 
86 T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead 
87 k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Bind b) u t) H12) in ((let 
88 H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u1 
89 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) 
90 (THead (Bind b) u t) H12) in ((let H15 \def (f_equal T T (\lambda (e: 
91 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | 
92 (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead (Bind b) u t) H12) in 
93 (\lambda (H16: (eq T u1 u)).(\lambda (H17: (eq K k (Bind b))).(eq_ind_r K 
94 (Bind b) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) a2)) (let H18 \def 
95 (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 
96 t4 a2))) H11 t H15) in (let H19 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 
97 t4)) H10 t H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).((eq T t0 
98 (THead (Bind b) u t)) \to (arity g c2 u2 a2))) H9 u H16) in (let H21 \def 
99 (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H16) in (arity_bind g b H0 c2 
100 u2 a1 (H2 c2 H5 u2 H21) t4 a2 (H4 (CHead c2 (Bind b) u2) (wcpr0_comp c c2 H5 
101 u u2 H21 (Bind b)) t4 H19)))))) k H17)))) H14)) H13)))))))))))) (\lambda (u0: 
102 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: 
103 (((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2 a2)))).(\lambda (t3: 
104 T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead 
105 (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H12: (eq T (THead (Flat 
106 Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Bind b) u t))).(let H13 \def 
107 (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: 
108 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
109 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
110 _) \Rightarrow True])])) I (THead (Bind b) u t) H12) in (False_ind (arity g 
111 c2 (THead (Bind Abbr) v2 t4) a2) H13)))))))))))) (\lambda (b0: B).(\lambda 
112 (_: (not (eq B b0 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 
113 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2 
114 a2)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda 
115 (_: (((eq T u1 (THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: 
116 T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead 
117 (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H15: (eq T (THead (Flat 
118 Appl) v1 (THead (Bind b0) u1 t3)) (THead (Bind b) u t))).(let H16 \def 
119 (eq_ind T (THead (Flat Appl) v1 (THead (Bind b0) u1 t3)) (\lambda (ee: 
120 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
121 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
122 _) \Rightarrow True])])) I (THead (Bind b) u t) H15) in (False_ind (arity g 
123 c2 (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2) 
124 H16))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (H8: (pr0 u1 
125 u2)).(\lambda (H9: (((eq T u1 (THead (Bind b) u t)) \to (arity g c2 u2 
126 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H10: (pr0 t3 t4)).(\lambda 
127 (H11: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (w: 
128 T).(\lambda (H12: (subst0 O u2 t4 w)).(\lambda (H13: (eq T (THead (Bind Abbr) 
129 u1 t3) (THead (Bind b) u t))).(let H14 \def (f_equal T B (\lambda (e: 
130 T).(match e with [(TSort _) \Rightarrow Abbr | (TLRef _) \Rightarrow Abbr | 
131 (THead k _ _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
132 \Rightarrow Abbr])])) (THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in 
133 ((let H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
134 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) 
135 (THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in ((let H16 \def 
136 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t3 | (TLRef 
137 _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) u1 
138 t3) (THead (Bind b) u t) H13) in (\lambda (H17: (eq T u1 u)).(\lambda (H18: 
139 (eq B Abbr b)).(let H19 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead 
140 (Bind b) u t)) \to (arity g c2 t4 a2))) H11 t H16) in (let H20 \def (eq_ind T 
141 t3 (\lambda (t0: T).(pr0 t0 t4)) H10 t H16) in (let H21 \def (eq_ind T u1 
142 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 u2 a2))) H9 
143 u H17) in (let H22 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H17) 
144 in (let H23 \def (eq_ind_r B b (\lambda (b0: B).((eq T t (THead (Bind b0) u 
145 t)) \to (arity g c2 t4 a2))) H19 Abbr H18) in (let H24 \def (eq_ind_r B b 
146 (\lambda (b0: B).((eq T u (THead (Bind b0) u t)) \to (arity g c2 u2 a2))) H21 
147 Abbr H18) in (let H25 \def (eq_ind_r B b (\lambda (b0: B).(\forall (c3: 
148 C).((wcpr0 (CHead c (Bind b0) u) c3) \to (\forall (t5: T).((pr0 t t5) \to 
149 (arity g c3 t5 a2)))))) H4 Abbr H18) in (let H26 \def (eq_ind_r B b (\lambda 
150 (b0: B).(arity g (CHead c (Bind b0) u) t a2)) H3 Abbr H18) in (let H27 \def 
151 (eq_ind_r B b (\lambda (b0: B).(not (eq B b0 Abst))) H0 Abbr H18) in 
152 (arity_bind g Abbr H27 c2 u2 a1 (H2 c2 H5 u2 H22) w a2 (arity_subst0 g (CHead 
153 c2 (Bind Abbr) u2) t4 a2 (H25 (CHead c2 (Bind Abbr) u2) (wcpr0_comp c c2 H5 u 
154 u2 H22 (Bind Abbr)) t4 H20) c2 u2 O (getl_refl Abbr c2 u2) w 
155 H12)))))))))))))) H15)) H14))))))))))))) (\lambda (b0: B).(\lambda (H8: (not 
156 (eq B b0 Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 
157 t4)).(\lambda (H10: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 
158 a2)))).(\lambda (u0: T).(\lambda (H11: (eq T (THead (Bind b0) u0 (lift (S O) 
159 O t3)) (THead (Bind b) u t))).(let H12 \def (f_equal T B (\lambda (e: 
160 T).(match e with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | 
161 (THead k _ _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat _) 
162 \Rightarrow b0])])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u 
163 t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort 
164 _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow 
165 t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t) H11) in 
166 ((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
167 \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _) 
168 \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _ 
169 t0) \Rightarrow t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) 
170 u t) H11) in (\lambda (_: (eq T u0 u)).(\lambda (H16: (eq B b0 b)).(let H17 
171 \def (eq_ind B b0 (\lambda (b1: B).(not (eq B b1 Abst))) H8 b H16) in (let 
172 H18 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Bind b) u t0)) \to 
173 (arity g c2 t4 a2))) H10 (lift (S O) O t3) H14) in (let H19 \def (eq_ind_r T 
174 t (\lambda (t0: T).(\forall (c3: C).((wcpr0 (CHead c (Bind b) u) c3) \to 
175 (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 a2)))))) H4 (lift (S O) O 
176 t3) H14) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).(arity g (CHead c 
177 (Bind b) u) t0 a2)) H3 (lift (S O) O t3) H14) in (arity_gen_lift g (CHead c2 
178 (Bind b) u) t4 a2 (S O) O (H19 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H5 u u 
179 (pr0_refl u) (Bind b)) (lift (S O) O t4) (pr0_lift t3 t4 H9 (S O) O)) c2 
180 (drop_drop (Bind b) O c2 c2 (drop_refl c2) u))))))))) H13)) H12)))))))))) 
181 (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: 
182 (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0: 
183 T).(\lambda (H10: (eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t))).(let 
184 H11 \def (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (ee: T).(match ee with 
185 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
186 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
187 True])])) I (THead (Bind b) u t) H10) in (False_ind (arity g c2 t4 a2) 
188 H11)))))))) y t2 H7))) H6)))))))))))))))) (\lambda (c: C).(\lambda (u: 
189 T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda (H1: 
190 ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 u t2) \to (arity g 
191 c2 t2 (asucc g a1)))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (H2: 
192 (arity g (CHead c (Bind Abst) u) t a2)).(\lambda (H3: ((\forall (c2: 
193 C).((wcpr0 (CHead c (Bind Abst) u) c2) \to (\forall (t2: T).((pr0 t t2) \to 
194 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c 
195 c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Bind Abst) u t) 
196 t2)).(insert_eq T (THead (Bind Abst) u t) (\lambda (t0: T).(pr0 t0 t2)) 
197 (\lambda (_: T).(arity g c2 t2 (AHead a1 a2))) (\lambda (y: T).(\lambda (H6: 
198 (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Bind 
199 Abst) u t)) \to (arity g c2 t3 (AHead a1 a2))))) (\lambda (t0: T).(\lambda 
200 (H7: (eq T t0 (THead (Bind Abst) u t))).(let H8 \def (f_equal T T (\lambda 
201 (e: T).e) t0 (THead (Bind Abst) u t) H7) in (eq_ind_r T (THead (Bind Abst) u 
202 t) (\lambda (t3: T).(arity g c2 t3 (AHead a1 a2))) (arity_head g c2 u a1 (H1 
203 c2 H4 u (pr0_refl u)) t a2 (H3 (CHead c2 (Bind Abst) u) (wcpr0_comp c c2 H4 u 
204 u (pr0_refl u) (Bind Abst)) t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
205 T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 
206 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2))))).(\lambda (t3: 
207 T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 
208 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (k: 
209 K).(\lambda (H11: (eq T (THead k u1 t3) (THead (Bind Abst) u t))).(let H12 
210 \def (f_equal T K (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | 
211 (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
212 (THead (Bind Abst) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: 
213 T).(match e with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | 
214 (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) (THead (Bind Abst) u t) H11) 
215 in ((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
216 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) 
217 (THead k u1 t3) (THead (Bind Abst) u t) H11) in (\lambda (H15: (eq T u1 
218 u)).(\lambda (H16: (eq K k (Bind Abst))).(eq_ind_r K (Bind Abst) (\lambda 
219 (k0: K).(arity g c2 (THead k0 u2 t4) (AHead a1 a2))) (let H17 \def (eq_ind T 
220 t3 (\lambda (t0: T).((eq T t0 (THead (Bind Abst) u t)) \to (arity g c2 t4 
221 (AHead a1 a2)))) H10 t H14) in (let H18 \def (eq_ind T t3 (\lambda (t0: 
222 T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind T u1 (\lambda (t0: T).((eq 
223 T t0 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2)))) H8 u H15) 
224 in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H7 u H15) in 
225 (arity_head g c2 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 (CHead c2 (Bind Abst) u2) 
226 (wcpr0_comp c c2 H4 u u2 H20 (Bind Abst)) t4 H18)))))) k H16)))) H13)) 
227 H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda 
228 (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) \to (arity 
229 g c2 v2 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
230 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
231 (AHead a1 a2))))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead (Bind 
232 Abst) u0 t3)) (THead (Bind Abst) u t))).(let H12 \def (eq_ind T (THead (Flat 
233 Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with [(TSort 
234 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
235 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
236 True])])) I (THead (Bind Abst) u t) H11) in (False_ind (arity g c2 (THead 
237 (Bind Abbr) v2 t4) (AHead a1 a2)) H12)))))))))))) (\lambda (b: B).(\lambda 
238 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 
239 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) \to (arity g c2 v2 
240 (AHead a1 a2))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 
241 u2)).(\lambda (_: (((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2 
242 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 
243 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
244 (AHead a1 a2))))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) 
245 u1 t3)) (THead (Bind Abst) u t))).(let H15 \def (eq_ind T (THead (Flat Appl) 
246 v1 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _) 
247 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
248 (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I 
249 (THead (Bind Abst) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 
250 (THead (Flat Appl) (lift (S O) O v2) t4)) (AHead a1 a2)) H15))))))))))))))))) 
251 (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: 
252 (((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 
253 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda 
254 (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 
255 a2))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T 
256 (THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t))).(let H13 \def (eq_ind T 
257 (THead (Bind Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _) 
258 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
259 (match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | 
260 Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow 
261 False])])) I (THead (Bind Abst) u t) H12) in (False_ind (arity g c2 (THead 
262 (Bind Abbr) u2 w) (AHead a1 a2)) H13))))))))))))) (\lambda (b: B).(\lambda 
263 (H7: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
264 t3 t4)).(\lambda (H9: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
265 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0 
266 (lift (S O) O t3)) (THead (Bind Abst) u t))).(let H11 \def (f_equal T B 
267 (\lambda (e: T).(match e with [(TSort _) \Rightarrow b | (TLRef _) 
268 \Rightarrow b | (THead k _ _) \Rightarrow (match k with [(Bind b0) 
269 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u0 (lift (S O) O 
270 t3)) (THead (Bind Abst) u t) H10) in ((let H12 \def (f_equal T T (\lambda (e: 
271 T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | 
272 (THead _ t0 _) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead 
273 (Bind Abst) u t) H10) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e 
274 with [(TSort _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) 
275 | (TLRef _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | 
276 (THead _ _ t0) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead 
277 (Bind Abst) u t) H10) in (\lambda (_: (eq T u0 u)).(\lambda (H15: (eq B b 
278 Abst)).(let H16 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H7 
279 Abst H15) in (let H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead 
280 (Bind Abst) u t0)) \to (arity g c2 t4 (AHead a1 a2)))) H9 (lift (S O) O t3) 
281 H13) in (let H18 \def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 
282 (CHead c (Bind Abst) u) c3) \to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 
283 t5 a2)))))) H3 (lift (S O) O t3) H13) in (let H19 \def (eq_ind_r T t (\lambda 
284 (t0: T).(arity g (CHead c (Bind Abst) u) t0 a2)) H2 (lift (S O) O t3) H13) in 
285 (let H20 \def (match (H16 (refl_equal B Abst)) in False with []) in 
286 H20)))))))) H12)) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda 
287 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity 
288 g c2 t4 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat 
289 Cast) u0 t3) (THead (Bind Abst) u t))).(let H10 \def (eq_ind T (THead (Flat 
290 Cast) u0 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
291 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind 
292 _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u 
293 t) H9) in (False_ind (arity g c2 t4 (AHead a1 a2)) H10)))))))) y t2 H6))) 
294 H5)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda 
295 (_: (arity g c u a1)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to 
296 (\forall (t2: T).((pr0 u t2) \to (arity g c2 t2 a1))))))).(\lambda (t: 
297 T).(\lambda (a2: A).(\lambda (H2: (arity g c t (AHead a1 a2))).(\lambda (H3: 
298 ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g 
299 c2 t2 (AHead a1 a2)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c 
300 c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Flat Appl) u t) 
301 t2)).(insert_eq T (THead (Flat Appl) u t) (\lambda (t0: T).(pr0 t0 t2)) 
302 (\lambda (_: T).(arity g c2 t2 a2)) (\lambda (y: T).(\lambda (H6: (pr0 y 
303 t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Flat Appl) 
304 u t)) \to (arity g c2 t3 a2)))) (\lambda (t0: T).(\lambda (H7: (eq T t0 
305 (THead (Flat Appl) u t))).(let H8 \def (f_equal T T (\lambda (e: T).e) t0 
306 (THead (Flat Appl) u t) H7) in (eq_ind_r T (THead (Flat Appl) u t) (\lambda 
307 (t3: T).(arity g c2 t3 a2)) (arity_appl g c2 u a1 (H1 c2 H4 u (pr0_refl u)) t 
308 a2 (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: T).(\lambda (u2: 
309 T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 (THead (Flat Appl) u 
310 t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: 
311 (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g 
312 c2 t4 a2)))).(\lambda (k: K).(\lambda (H11: (eq T (THead k u1 t3) (THead 
313 (Flat Appl) u t))).(let H12 \def (f_equal T K (\lambda (e: T).(match e with 
314 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) 
315 \Rightarrow k0])) (THead k u1 t3) (THead (Flat Appl) u t) H11) in ((let H13 
316 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u1 | 
317 (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) 
318 (THead (Flat Appl) u t) H11) in ((let H14 \def (f_equal T T (\lambda (e: 
319 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | 
320 (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead (Flat Appl) u t) H11) 
321 in (\lambda (H15: (eq T u1 u)).(\lambda (H16: (eq K k (Flat Appl))).(eq_ind_r 
322 K (Flat Appl) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) a2)) (let H17 
323 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to 
324 (arity g c2 t4 a2))) H10 t H14) in (let H18 \def (eq_ind T t3 (\lambda (t0: 
325 T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind T u1 (\lambda (t0: T).((eq 
326 T t0 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2))) H8 u H15) in (let H20 
327 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H7 u H15) in (arity_appl g c2 
328 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 c2 H4 t4 H18)))))) k H16)))) H13)) 
329 H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda 
330 (H7: (pr0 v1 v2)).(\lambda (H8: (((eq T v1 (THead (Flat Appl) u t)) \to 
331 (arity g c2 v2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 
332 t4)).(\lambda (H10: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 
333 a2)))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) 
334 (THead (Flat Appl) u t))).(let H12 \def (f_equal T T (\lambda (e: T).(match e 
335 with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t0 _) 
336 \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead 
337 (Flat Appl) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e 
338 with [(TSort _) \Rightarrow (THead (Bind Abst) u0 t3) | (TLRef _) \Rightarrow 
339 (THead (Bind Abst) u0 t3) | (THead _ _ t0) \Rightarrow t0])) (THead (Flat 
340 Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) u t) H11) in (\lambda 
341 (H14: (eq T v1 u)).(let H15 \def (eq_ind T v1 (\lambda (t0: T).((eq T t0 
342 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2))) H8 u H14) in (let H16 \def 
343 (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2)) H7 u H14) in (let H17 \def 
344 (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Flat Appl) u t0)) \to (arity 
345 g c2 t4 a2))) H10 (THead (Bind Abst) u0 t3) H13) in (let H18 \def (eq_ind_r T 
346 t (\lambda (t0: T).((eq T u (THead (Flat Appl) u t0)) \to (arity g c2 v2 
347 a2))) H15 (THead (Bind Abst) u0 t3) H13) in (let H19 \def (eq_ind_r T t 
348 (\lambda (t0: T).(\forall (c3: C).((wcpr0 c c3) \to (\forall (t5: T).((pr0 t0 
349 t5) \to (arity g c3 t5 (AHead a1 a2))))))) H3 (THead (Bind Abst) u0 t3) H13) 
350 in (let H20 \def (eq_ind_r T t (\lambda (t0: T).(arity g c t0 (AHead a1 a2))) 
351 H2 (THead (Bind Abst) u0 t3) H13) in (let H21 \def (H1 c2 H4 v2 H16) in (let 
352 H22 \def (H19 c2 H4 (THead (Bind Abst) u0 t4) (pr0_comp u0 u0 (pr0_refl u0) 
353 t3 t4 H9 (Bind Abst))) in (let H23 \def (arity_gen_abst g c2 u0 t4 (AHead a1 
354 a2) H22) in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq A (AHead a1 
355 a2) (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c2 u0 (asucc g 
356 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c2 (Bind Abst) u0) t4 
357 a4))) (arity g c2 (THead (Bind Abbr) v2 t4) a2) (\lambda (x0: A).(\lambda 
358 (x1: A).(\lambda (H24: (eq A (AHead a1 a2) (AHead x0 x1))).(\lambda (H25: 
359 (arity g c2 u0 (asucc g x0))).(\lambda (H26: (arity g (CHead c2 (Bind Abst) 
360 u0) t4 x1)).(let H27 \def (f_equal A A (\lambda (e: A).(match e with [(ASort 
361 _ _) \Rightarrow a1 | (AHead a0 _) \Rightarrow a0])) (AHead a1 a2) (AHead x0 
362 x1) H24) in ((let H28 \def (f_equal A A (\lambda (e: A).(match e with [(ASort 
363 _ _) \Rightarrow a2 | (AHead _ a0) \Rightarrow a0])) (AHead a1 a2) (AHead x0 
364 x1) H24) in (\lambda (H29: (eq A a1 x0)).(let H30 \def (eq_ind_r A x1 
365 (\lambda (a0: A).(arity g (CHead c2 (Bind Abst) u0) t4 a0)) H26 a2 H28) in 
366 (let H31 \def (eq_ind_r A x0 (\lambda (a0: A).(arity g c2 u0 (asucc g a0))) 
367 H25 a1 H29) in (arity_bind g Abbr not_abbr_abst c2 v2 a1 H21 t4 a2 
368 (csuba_arity g (CHead c2 (Bind Abst) u0) t4 a2 H30 (CHead c2 (Bind Abbr) v2) 
369 (csuba_abst g c2 c2 (csuba_refl g c2) u0 a1 H31 v2 H21))))))) H27))))))) 
370 H23)))))))))))) H12)))))))))))) (\lambda (b: B).(\lambda (H7: (not (eq B b 
371 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H8: (pr0 v1 v2)).(\lambda 
372 (H9: (((eq T v1 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2)))).(\lambda 
373 (u1: T).(\lambda (u2: T).(\lambda (H10: (pr0 u1 u2)).(\lambda (H11: (((eq T 
374 u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: 
375 T).(\lambda (t4: T).(\lambda (H12: (pr0 t3 t4)).(\lambda (H13: (((eq T t3 
376 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (H14: (eq T 
377 (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t))).(let 
378 H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v1 
379 | (TLRef _) \Rightarrow v1 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat 
380 Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t) H14) in ((let H16 
381 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead 
382 (Bind b) u1 t3) | (TLRef _) \Rightarrow (THead (Bind b) u1 t3) | (THead _ _ 
383 t0) \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead 
384 (Flat Appl) u t) H14) in (\lambda (H17: (eq T v1 u)).(let H18 \def (eq_ind T 
385 v1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 v2 
386 a2))) H9 u H17) in (let H19 \def (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2)) 
387 H8 u H17) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead 
388 (Flat Appl) u t0)) \to (arity g c2 t4 a2))) H13 (THead (Bind b) u1 t3) H16) 
389 in (let H21 \def (eq_ind_r T t (\lambda (t0: T).((eq T u1 (THead (Flat Appl) 
390 u t0)) \to (arity g c2 u2 a2))) H11 (THead (Bind b) u1 t3) H16) in (let H22 
391 \def (eq_ind_r T t (\lambda (t0: T).((eq T u (THead (Flat Appl) u t0)) \to 
392 (arity g c2 v2 a2))) H18 (THead (Bind b) u1 t3) H16) in (let H23 \def 
393 (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 c c3) \to (\forall 
394 (t5: T).((pr0 t0 t5) \to (arity g c3 t5 (AHead a1 a2))))))) H3 (THead (Bind 
395 b) u1 t3) H16) in (let H24 \def (eq_ind_r T t (\lambda (t0: T).(arity g c t0 
396 (AHead a1 a2))) H2 (THead (Bind b) u1 t3) H16) in (let H25 \def (H1 c2 H4 v2 
397 H19) in (let H26 \def (H23 c2 H4 (THead (Bind b) u2 t4) (pr0_comp u1 u2 H10 
398 t3 t4 H12 (Bind b))) in (let H27 \def (arity_gen_bind b H7 g c2 u2 t4 (AHead 
399 a1 a2) H26) in (ex2_ind A (\lambda (a3: A).(arity g c2 u2 a3)) (\lambda (_: 
400 A).(arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2))) (arity g c2 (THead 
401 (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2) (\lambda (x: 
402 A).(\lambda (H28: (arity g c2 u2 x)).(\lambda (H29: (arity g (CHead c2 (Bind 
403 b) u2) t4 (AHead a1 a2))).(arity_bind g b H7 c2 u2 x H28 (THead (Flat Appl) 
404 (lift (S O) O v2) t4) a2 (arity_appl g (CHead c2 (Bind b) u2) (lift (S O) O 
405 v2) a1 (arity_lift g c2 v2 a1 H25 (CHead c2 (Bind b) u2) (S O) O (drop_drop 
406 (Bind b) O c2 c2 (drop_refl c2) u2)) t4 a2 H29))))) H27))))))))))))) 
407 H15))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 
408 u2)).(\lambda (_: (((eq T u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 
409 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda 
410 (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda 
411 (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T (THead (Bind 
412 Abbr) u1 t3) (THead (Flat Appl) u t))).(let H13 \def (eq_ind T (THead (Bind 
413 Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
414 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind 
415 _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u 
416 t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) u2 w) a2) 
417 H13))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
418 (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 
419 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0: T).(\lambda 
420 (H10: (eq T (THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Appl) u 
421 t))).(let H11 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O t3)) (\lambda 
422 (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow 
423 False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | 
424 (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u t) H10) in (False_ind 
425 (arity g c2 t4 a2) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda 
426 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity 
427 g c2 t4 a2)))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat Cast) u0 t3) 
428 (THead (Flat Appl) u t))).(let H10 \def (eq_ind T (THead (Flat Cast) u0 t3) 
429 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
430 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
431 \Rightarrow False | (Flat f) \Rightarrow (match f with [Appl \Rightarrow 
432 False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t) H9) in 
433 (False_ind (arity g c2 t4 a2) H10)))))))) y t2 H6))) H5)))))))))))))) 
434 (\lambda (c: C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c u 
435 (asucc g a0))).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall 
436 (t2: T).((pr0 u t2) \to (arity g c2 t2 (asucc g a0)))))))).(\lambda (t: 
437 T).(\lambda (_: (arity g c t a0)).(\lambda (H3: ((\forall (c2: C).((wcpr0 c 
438 c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 a0))))))).(\lambda 
439 (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H5: (pr0 
440 (THead (Flat Cast) u t) t2)).(insert_eq T (THead (Flat Cast) u t) (\lambda 
441 (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g c2 t2 a0)) (\lambda (y: 
442 T).(\lambda (H6: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq 
443 T t0 (THead (Flat Cast) u t)) \to (arity g c2 t3 a0)))) (\lambda (t0: 
444 T).(\lambda (H7: (eq T t0 (THead (Flat Cast) u t))).(let H8 \def (f_equal T T 
445 (\lambda (e: T).e) t0 (THead (Flat Cast) u t) H7) in (eq_ind_r T (THead (Flat 
446 Cast) u t) (\lambda (t3: T).(arity g c2 t3 a0)) (arity_cast g c2 u a0 (H1 c2 
447 H4 u (pr0_refl u)) t (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
448 T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 
449 (THead (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda 
450 (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat 
451 Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (k: K).(\lambda (H11: (eq T 
452 (THead k u1 t3) (THead (Flat Cast) u t))).(let H12 \def (f_equal T K (\lambda 
453 (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | 
454 (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Flat Cast) u t) H11) 
455 in ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
456 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) 
457 (THead k u1 t3) (THead (Flat Cast) u t) H11) in ((let H14 \def (f_equal T T 
458 (\lambda (e: T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) 
459 \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead 
460 (Flat Cast) u t) H11) in (\lambda (H15: (eq T u1 u)).(\lambda (H16: (eq K k 
461 (Flat Cast))).(eq_ind_r K (Flat Cast) (\lambda (k0: K).(arity g c2 (THead k0 
462 u2 t4) a0)) (let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead 
463 (Flat Cast) u t)) \to (arity g c2 t4 a0))) H10 t H14) in (let H18 \def 
464 (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind 
465 T u1 (\lambda (t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 u2 
466 a0))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) 
467 H7 u H15) in (arity_cast g c2 u2 a0 (H1 c2 H4 u2 H20) t4 (H3 c2 H4 t4 
468 H18)))))) k H16)))) H13)) H12)))))))))))) (\lambda (u0: T).(\lambda (v1: 
469 T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead 
470 (Flat Cast) u t)) \to (arity g c2 v2 a0)))).(\lambda (t3: T).(\lambda (t4: 
471 T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) 
472 \to (arity g c2 t4 a0)))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead 
473 (Bind Abst) u0 t3)) (THead (Flat Cast) u t))).(let H12 \def (eq_ind T (THead 
474 (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with 
475 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
476 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow 
477 (match f with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead 
478 (Flat Cast) u t) H11) in (False_ind (arity g c2 (THead (Bind Abbr) v2 t4) a0) 
479 H12)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
480 (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 
481 (THead (Flat Cast) u t)) \to (arity g c2 v2 a0)))).(\lambda (u1: T).(\lambda 
482 (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Flat Cast) 
483 u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda 
484 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity 
485 g c2 t4 a0)))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 
486 t3)) (THead (Flat Cast) u t))).(let H15 \def (eq_ind T (THead (Flat Appl) v1 
487 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _) 
488 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
489 (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f 
490 with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat 
491 Cast) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 (THead (Flat 
492 Appl) (lift (S O) O v2) t4)) a0) H15))))))))))))))))) (\lambda (u1: 
493 T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead 
494 (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: 
495 T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) 
496 \to (arity g c2 t4 a0)))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 
497 w)).(\lambda (H12: (eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u 
498 t))).(let H13 \def (eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (ee: 
499 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
500 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat 
501 _) \Rightarrow False])])) I (THead (Flat Cast) u t) H12) in (False_ind (arity 
502 g c2 (THead (Bind Abbr) u2 w) a0) H13))))))))))))) (\lambda (b: B).(\lambda 
503 (_: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
504 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity g c2 t4 
505 a0)))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0 (lift (S O) O 
506 t3)) (THead (Flat Cast) u t))).(let H11 \def (eq_ind T (THead (Bind b) u0 
507 (lift (S O) O t3)) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow 
508 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with 
509 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
510 Cast) u t) H10) in (False_ind (arity g c2 t4 a0) H11)))))))))) (\lambda (t3: 
511 T).(\lambda (t4: T).(\lambda (H7: (pr0 t3 t4)).(\lambda (H8: (((eq T t3 
512 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (u0: T).(\lambda 
513 (H9: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t))).(let H10 \def 
514 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef 
515 _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Cast) u0 
516 t3) (THead (Flat Cast) u t) H9) in ((let H11 \def (f_equal T T (\lambda (e: 
517 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | 
518 (THead _ _ t0) \Rightarrow t0])) (THead (Flat Cast) u0 t3) (THead (Flat Cast) 
519 u t) H9) in (\lambda (_: (eq T u0 u)).(let H13 \def (eq_ind T t3 (\lambda 
520 (t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0))) H8 t H11) 
521 in (let H14 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H7 t H11) in (H3 
522 c2 H4 t4 H14))))) H10)))))))) y t2 H6))) H5))))))))))))) (\lambda (c: 
523 C).(\lambda (t: T).(\lambda (a1: A).(\lambda (_: (arity g c t a1)).(\lambda 
524 (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to 
525 (arity g c2 t2 a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 
526 a2)).(\lambda (c2: C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda 
527 (H4: (pr0 t t2)).(arity_repl g c2 t2 a1 (H1 c2 H3 t2 H4) a2 H2)))))))))))) c1 
528 t1 a H))))).
529
530 lemma arity_sred_wcpr0_pr1:
531  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall 
532 (c1: C).(\forall (a: A).((arity g c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 
533 c2) \to (arity g c2 t2 a)))))))))
534 \def
535  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1 t2)).(pr1_ind (\lambda 
536 (t: T).(\lambda (t0: T).(\forall (g: G).(\forall (c1: C).(\forall (a: 
537 A).((arity g c1 t a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (arity g c2 t0 
538 a))))))))) (\lambda (t: T).(\lambda (g: G).(\lambda (c1: C).(\lambda (a: 
539 A).(\lambda (H0: (arity g c1 t a)).(\lambda (c2: C).(\lambda (H1: (wcpr0 c1 
540 c2)).(arity_sred_wcpr0_pr0 g c1 t a H0 c2 H1 t (pr0_refl t))))))))) (\lambda 
541 (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t4 t3)).(\lambda (t5: T).(\lambda 
542 (_: (pr1 t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (c1: C).(\forall (a: 
543 A).((arity g c1 t3 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (arity g c2 t5 
544 a))))))))).(\lambda (g: G).(\lambda (c1: C).(\lambda (a: A).(\lambda (H3: 
545 (arity g c1 t4 a)).(\lambda (c2: C).(\lambda (H4: (wcpr0 c1 c2)).(H2 g c2 a 
546 (arity_sred_wcpr0_pr0 g c1 t4 a H3 c2 H4 t3 H0) c2 (wcpr0_refl 
547 c2)))))))))))))) t1 t2 H))).
548
549 lemma arity_sred_pr2:
550  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
551 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
552 \def
553  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1 
554 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (g: 
555 G).(\forall (a: A).((arity g c0 t a) \to (arity g c0 t0 a))))))) (\lambda 
556 (c0: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda 
557 (g: G).(\lambda (a: A).(\lambda (H1: (arity g c0 t3 a)).(arity_sred_wcpr0_pr0 
558 g c0 t3 a H1 c0 (wcpr0_refl c0) t4 H0)))))))) (\lambda (c0: C).(\lambda (d: 
559 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind 
560 Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 
561 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g: 
562 G).(\lambda (a: A).(\lambda (H3: (arity g c0 t3 a)).(arity_subst0 g c0 t4 a 
563 (arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t 
564 H2)))))))))))))) c t1 t2 H)))).
565
566 lemma arity_sred_pr3:
567  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
568 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
569 \def
570  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1 
571 t2)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (g: G).(\forall (a: 
572 A).((arity g c t a) \to (arity g c t0 a)))))) (\lambda (t: T).(\lambda (g: 
573 G).(\lambda (a: A).(\lambda (H0: (arity g c t a)).H0)))) (\lambda (t3: 
574 T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda 
575 (_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (a: A).((arity g c 
576 t3 a) \to (arity g c t5 a)))))).(\lambda (g: G).(\lambda (a: A).(\lambda (H3: 
577 (arity g c t4 a)).(H2 g a (arity_sred_pr2 c t4 t3 H0 g a H3))))))))))) t1 t2 
578 H)))).
579