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