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