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