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