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