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