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