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