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