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).(and_ind (eq nat i i0) (eq T v (lift (S i) O
53 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).(and_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 H2 \def (fsubst0_gen_base c c2 (TSort
274 n) t2 u i H1) in (or3_ind (land (eq C c c2) (subst0 i u (TSort n) t2)) (land
275 (eq T (TSort n) t2) (csubst0 i u c c2)) (land (subst0 i u (TSort n) t2)
276 (csubst0 i u c c2)) (arity g c2 t2 (ASort O n)) (\lambda (H3: (land (eq C c
277 c2) (subst0 i u (TSort n) t2))).(and_ind (eq C c c2) (subst0 i u (TSort n)
278 t2) (arity g c2 t2 (ASort O n)) (\lambda (H4: (eq C c c2)).(\lambda (H5:
279 (subst0 i u (TSort n) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 (ASort
280 O n))) (subst0_gen_sort u t2 i n H5 (arity g c t2 (ASort O n))) c2 H4))) H3))
281 (\lambda (H3: (land (eq T (TSort n) t2) (csubst0 i u c c2))).(and_ind (eq T
282 (TSort n) t2) (csubst0 i u c c2) (arity g c2 t2 (ASort O n)) (\lambda (H4:
283 (eq T (TSort n) t2)).(\lambda (_: (csubst0 i u c c2)).(eq_ind T (TSort n)
284 (\lambda (t: T).(arity g c2 t (ASort O n))) (arity_sort g c2 n) t2 H4))) H3))
285 (\lambda (H3: (land (subst0 i u (TSort n) t2) (csubst0 i u c c2))).(and_ind
286 (subst0 i u (TSort n) t2) (csubst0 i u c c2) (arity g c2 t2 (ASort O n))
287 (\lambda (H4: (subst0 i u (TSort n) t2)).(\lambda (_: (csubst0 i u c
288 c2)).(subst0_gen_sort u t2 i n H4 (arity g c2 t2 (ASort O n))))) H3))
289 H2))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i:
290 nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (a0:
291 A).(\lambda (H1: (arity g d u a0)).(\lambda (H2: ((\forall (d1: C).(\forall
292 (u0: T).(\forall (i0: nat).((getl i0 d (CHead d1 (Bind Abbr) u0)) \to
293 (\forall (c2: C).(\forall (t2: T).((fsubst0 i0 u0 d u c2 t2) \to (arity g c2
294 t2 a0)))))))))).(\lambda (d1: C).(\lambda (u0: T).(\lambda (i0: nat).(\lambda
295 (H3: (getl i0 c (CHead d1 (Bind Abbr) u0))).(\lambda (c2: C).(\lambda (t2:
296 T).(\lambda (H4: (fsubst0 i0 u0 c (TLRef i) c2 t2)).(let H5 \def
297 (fsubst0_gen_base c c2 (TLRef i) t2 u0 i0 H4) in (or3_ind (land (eq C c c2)
298 (subst0 i0 u0 (TLRef i) t2)) (land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2))
299 (land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2)) (arity g c2 t2 a0)
300 (\lambda (H6: (land (eq C c c2) (subst0 i0 u0 (TLRef i) t2))).(and_ind (eq C
301 c c2) (subst0 i0 u0 (TLRef i) t2) (arity g c2 t2 a0) (\lambda (H7: (eq C c
302 c2)).(\lambda (H8: (subst0 i0 u0 (TLRef i) t2)).(eq_ind C c (\lambda (c0:
303 C).(arity g c0 t2 a0)) (and_ind (eq nat i i0) (eq T t2 (lift (S i) O u0))
304 (arity g c t2 a0) (\lambda (H9: (eq nat i i0)).(\lambda (H10: (eq T t2 (lift
305 (S i) O u0))).(eq_ind_r T (lift (S i) O u0) (\lambda (t: T).(arity g c t a0))
306 (let H11 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d1 (Bind
307 Abbr) u0))) H3 i H9) in (let H12 \def (eq_ind C (CHead d (Bind Abbr) u)
308 (\lambda (c0: C).(getl i c c0)) H0 (CHead d1 (Bind Abbr) u0) (getl_mono c
309 (CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind Abbr) u0) H11)) in (let H13 \def
310 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
311 [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind
312 Abbr) u) (CHead d1 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H0
313 (CHead d1 (Bind Abbr) u0) H11)) in ((let H14 \def (f_equal C T (\lambda (e:
314 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
315 (CHead _ _ t) \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr)
316 u0) (getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind Abbr) u0) H11))
317 in (\lambda (H15: (eq C d d1)).(let H16 \def (eq_ind_r T u0 (\lambda (t:
318 T).(getl i c (CHead d1 (Bind Abbr) t))) H12 u H14) in (eq_ind T u (\lambda
319 (t: T).(arity g c (lift (S i) O t) a0)) (let H17 \def (eq_ind_r C d1 (\lambda
320 (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H16 d H15) in (arity_lift g d u
321 a0 H1 c (S i) O (getl_drop Abbr c d u i H17))) u0 H14)))) H13)))) t2 H10)))
322 (subst0_gen_lref u0 t2 i0 i H8)) c2 H7))) H6)) (\lambda (H6: (land (eq T
323 (TLRef i) t2) (csubst0 i0 u0 c c2))).(and_ind (eq T (TLRef i) t2) (csubst0 i0
324 u0 c c2) (arity g c2 t2 a0) (\lambda (H7: (eq T (TLRef i) t2)).(\lambda (H8:
325 (csubst0 i0 u0 c c2)).(eq_ind T (TLRef i) (\lambda (t: T).(arity g c2 t a0))
326 (lt_le_e i i0 (arity g c2 (TLRef i) a0) (\lambda (H9: (lt i i0)).(let H10
327 \def (csubst0_getl_lt i0 i H9 c c2 u0 H8 (CHead d (Bind Abbr) u) H0) in
328 (or4_ind (getl i c2 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b:
329 B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind
330 Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0:
331 C).(\lambda (_: T).(\lambda (w: T).(getl i c2 (CHead e0 (Bind b) w))))))
332 (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
333 (minus i0 (S i)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1:
334 C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
335 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
336 (u1: T).(getl i c2 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1:
337 C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
338 (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
339 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
340 u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
341 T).(\lambda (w: T).(getl i c2 (CHead e2 (Bind b) w))))))) (\lambda (_:
342 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
343 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
344 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))
345 (arity g c2 (TLRef i) a0) (\lambda (H11: (getl i c2 (CHead d (Bind Abbr)
346 u))).(let H12 \def (eq_ind nat (minus i0 i) (\lambda (n: nat).(getl n (CHead
347 d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0))) (getl_conf_le i0 (CHead d1 (Bind
348 Abbr) u0) c H3 (CHead d (Bind Abbr) u) i H0 (le_S_n i i0 (le_S (S i) i0 H9)))
349 (S (minus i0 (S i))) (minus_x_Sy i0 i H9)) in (arity_abbr g c2 d u i H11 a0
350 H1))) (\lambda (H11: (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda
351 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b)
352 u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
353 T).(getl i c2 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_:
354 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1
355 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1:
356 T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1))))))
357 (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c2
358 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: C).(\lambda (u1:
359 T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))) (arity g c2 (TLRef
360 i) a0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (x3:
361 T).(\lambda (H12: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
362 x2))).(\lambda (H13: (getl i c2 (CHead x1 (Bind x0) x3))).(\lambda (H14:
363 (subst0 (minus i0 (S i)) u0 x2 x3)).(let H15 \def (eq_ind nat (minus i0 i)
364 (\lambda (n: nat).(getl n (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)))
365 (getl_conf_le i0 (CHead d1 (Bind Abbr) u0) c H3 (CHead d (Bind Abbr) u) i H0
366 (le_S_n i i0 (le_S (S i) i0 H9))) (S (minus i0 (S i))) (minus_x_Sy i0 i H9))
367 in (let H16 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
368 (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0]))
369 (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H12) in ((let H17 \def
370 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
371 [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k in K return
372 (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
373 Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H12) in ((let H18
374 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
375 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead d (Bind
376 Abbr) u) (CHead x1 (Bind x0) x2) H12) in (\lambda (H19: (eq B Abbr
377 x0)).(\lambda (H20: (eq C d x1)).(let H21 \def (eq_ind_r T x2 (\lambda (t:
378 T).(subst0 (minus i0 (S i)) u0 t x3)) H14 u H18) in (let H22 \def (eq_ind_r C
379 x1 (\lambda (c0: C).(getl i c2 (CHead c0 (Bind x0) x3))) H13 d H20) in (let
380 H23 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c2 (CHead d (Bind b) x3)))
381 H22 Abbr H19) in (arity_abbr g c2 d x3 i H23 a0 (H2 d1 u0 (r (Bind Abbr)
382 (minus i0 (S i))) (getl_gen_S (Bind Abbr) d (CHead d1 (Bind Abbr) u0) u
383 (minus i0 (S i)) H15) d x3 (fsubst0_snd (r (Bind Abbr) (minus i0 (S i))) u0 d
384 u x3 H21))))))))) H17)) H16)))))))))) H11)) (\lambda (H11: (ex3_4 B C C T
385 (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
386 (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
387 (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c2 (CHead e2 (Bind b)
388 u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
389 T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
390 B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
391 Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
392 (e2: C).(\lambda (u1: T).(getl i c2 (CHead e2 (Bind b) u1)))))) (\lambda (_:
393 B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
394 i)) u0 e1 e2))))) (arity g c2 (TLRef i) a0) (\lambda (x0: B).(\lambda (x1:
395 C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H12: (eq C (CHead d (Bind
396 Abbr) u) (CHead x1 (Bind x0) x3))).(\lambda (H13: (getl i c2 (CHead x2 (Bind
397 x0) x3))).(\lambda (H14: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H15 \def
398 (eq_ind nat (minus i0 i) (\lambda (n: nat).(getl n (CHead d (Bind Abbr) u)
399 (CHead d1 (Bind Abbr) u0))) (getl_conf_le i0 (CHead d1 (Bind Abbr) u0) c H3
400 (CHead d (Bind Abbr) u) i H0 (le_S_n i i0 (le_S (S i) i0 H9))) (S (minus i0
401 (S i))) (minus_x_Sy i0 i H9)) in (let H16 \def (f_equal C C (\lambda (e:
402 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
403 (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
404 x3) H12) in ((let H17 \def (f_equal C B (\lambda (e: C).(match e in C return
405 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
406 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
407 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
408 x1 (Bind x0) x3) H12) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e
409 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
410 \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H12) in
411 (\lambda (H19: (eq B Abbr x0)).(\lambda (H20: (eq C d x1)).(let H21 \def
412 (eq_ind_r T x3 (\lambda (t: T).(getl i c2 (CHead x2 (Bind x0) t))) H13 u H18)
413 in (let H22 \def (eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i0 (S i)) u0
414 c0 x2)) H14 d H20) in (let H23 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c2
415 (CHead x2 (Bind b) u))) H21 Abbr H19) in (arity_abbr g c2 x2 u i H23 a0 (H2
416 d1 u0 (r (Bind Abbr) (minus i0 (S i))) (getl_gen_S (Bind Abbr) d (CHead d1
417 (Bind Abbr) u0) u (minus i0 (S i)) H15) x2 u (fsubst0_fst (r (Bind Abbr)
418 (minus i0 (S i))) u0 d u x2 H22))))))))) H17)) H16)))))))))) H11)) (\lambda
419 (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))).(and_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)).(and_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 H5
494 \def (fsubst0_gen_base c c2 (TLRef i) t2 u0 i0 H4) in (or3_ind (land (eq C c
495 c2) (subst0 i0 u0 (TLRef i) t2)) (land (eq T (TLRef i) t2) (csubst0 i0 u0 c
496 c2)) (land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2)) (arity g c2 t2
497 a0) (\lambda (H6: (land (eq C c c2) (subst0 i0 u0 (TLRef i) t2))).(and_ind
498 (eq C c c2) (subst0 i0 u0 (TLRef i) t2) (arity g c2 t2 a0) (\lambda (H7: (eq
499 C c c2)).(\lambda (H8: (subst0 i0 u0 (TLRef i) t2)).(eq_ind C c (\lambda (c0:
500 C).(arity g c0 t2 a0)) (and_ind (eq nat i i0) (eq T t2 (lift (S i) O u0))
501 (arity g c t2 a0) (\lambda (H9: (eq nat i i0)).(\lambda (H10: (eq T t2 (lift
502 (S i) O u0))).(eq_ind_r T (lift (S i) O u0) (\lambda (t: T).(arity g c t a0))
503 (let H11 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d1 (Bind
504 Abbr) u0))) H3 i H9) in (let H12 \def (eq_ind C (CHead d (Bind Abst) u)
505 (\lambda (c0: C).(getl i c c0)) H0 (CHead d1 (Bind Abbr) u0) (getl_mono c
506 (CHead d (Bind Abst) u) i H0 (CHead d1 (Bind Abbr) u0) H11)) in (let H13 \def
507 (eq_ind C (CHead d (Bind Abst) u) (\lambda (ee: C).(match ee in C return
508 (\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))).(and_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))).(and_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)).(and_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 H7 \def (fsubst0_gen_base c c2 (THead (Bind b) u
684 t) t2 u0 i H6) in (or3_ind (land (eq C c c2) (subst0 i u0 (THead (Bind b) u
685 t) t2)) (land (eq T (THead (Bind b) u t) t2) (csubst0 i u0 c c2)) (land
686 (subst0 i u0 (THead (Bind b) u t) t2) (csubst0 i u0 c c2)) (arity g c2 t2 a2)
687 (\lambda (H8: (land (eq C c c2) (subst0 i u0 (THead (Bind b) u t)
688 t2))).(and_ind (eq C c c2) (subst0 i u0 (THead (Bind b) u t) t2) (arity g c2
689 t2 a2) (\lambda (H9: (eq C c c2)).(\lambda (H10: (subst0 i u0 (THead (Bind b)
690 u t) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 a2)) (or3_ind (ex2 T
691 (\lambda (u2: T).(eq T t2 (THead (Bind b) u2 t))) (\lambda (u2: T).(subst0 i
692 u0 u u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))) (\lambda
693 (t3: T).(subst0 (s (Bind b) i) u0 t t3))) (ex3_2 T T (\lambda (u2:
694 T).(\lambda (t3: T).(eq T t2 (THead (Bind b) u2 t3)))) (\lambda (u2:
695 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))).(and_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))).(and_ind (subst0 i u0 (THead (Bind b) u t) t2) (csubst0
741 i u0 c c2) (arity g c2 t2 a2) (\lambda (H9: (subst0 i u0 (THead (Bind b) u t)
742 t2)).(\lambda (H10: (csubst0 i u0 c c2)).(or3_ind (ex2 T (\lambda (u2: T).(eq
743 T t2 (THead (Bind b) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T
744 (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))) (\lambda (t3: T).(subst0 (s
745 (Bind b) i) u0 t t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
746 (THead (Bind b) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u
747 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s (Bind b) i) u0 t t3))))
748 (arity g c2 t2 a2) (\lambda (H11: (ex2 T (\lambda (u2: T).(eq T t2 (THead
749 (Bind b) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2)))).(ex2_ind T (\lambda
750 (u2: T).(eq T t2 (THead (Bind b) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2))
751 (arity g c2 t2 a2) (\lambda (x: T).(\lambda (H12: (eq T t2 (THead (Bind b) x
752 t))).(\lambda (H13: (subst0 i u0 u x)).(eq_ind_r T (THead (Bind b) x t)
753 (\lambda (t0: T).(arity g c2 t0 a2)) (arity_bind g b H0 c2 x a1 (H2 d1 u0 i
754 H5 c2 x (fsubst0_both i u0 c u x H13 c2 H10)) t a2 (H4 d1 u0 (S i)
755 (getl_clear_bind b (CHead c (Bind b) u) c u (clear_bind b c u) (CHead d1
756 (Bind Abbr) u0) i H5) (CHead c2 (Bind b) x) t (fsubst0_fst (S i) u0 (CHead c
757 (Bind b) u) t (CHead c2 (Bind b) x) (csubst0_both_bind b i u0 u x H13 c c2
758 H10)))) t2 H12)))) H11)) (\lambda (H11: (ex2 T (\lambda (t3: T).(eq T t2
759 (THead (Bind b) u t3))) (\lambda (t3: T).(subst0 (s (Bind b) i) u0 t
760 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))) (\lambda
761 (t3: T).(subst0 (s (Bind b) i) u0 t t3)) (arity g c2 t2 a2) (\lambda (x:
762 T).(\lambda (H12: (eq T t2 (THead (Bind b) u x))).(\lambda (H13: (subst0 (s
763 (Bind b) i) u0 t x)).(eq_ind_r T (THead (Bind b) u x) (\lambda (t0: T).(arity
764 g c2 t0 a2)) (arity_bind g b H0 c2 u a1 (H2 d1 u0 i H5 c2 u (fsubst0_fst i u0
765 c u c2 H10)) x a2 (H4 d1 u0 (S i) (getl_clear_bind b (CHead c (Bind b) u) c u
766 (clear_bind b c u) (CHead d1 (Bind Abbr) u0) i H5) (CHead c2 (Bind b) u) x
767 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t x H13 (CHead c2 (Bind b) u)
768 (csubst0_fst_bind b i c c2 u0 H10 u)))) t2 H12)))) H11)) (\lambda (H11:
769 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) u2
770 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_:
771 T).(\lambda (t3: T).(subst0 (s (Bind b) i) u0 t t3))))).(ex3_2_ind T T
772 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) u2 t3)))) (\lambda
773 (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t3:
774 T).(subst0 (s (Bind b) i) u0 t t3))) (arity g c2 t2 a2) (\lambda (x0:
775 T).(\lambda (x1: T).(\lambda (H12: (eq T t2 (THead (Bind b) x0 x1))).(\lambda
776 (H13: (subst0 i u0 u x0)).(\lambda (H14: (subst0 (s (Bind b) i) u0 t
777 x1)).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t0: T).(arity g c2 t0 a2))
778 (arity_bind g b H0 c2 x0 a1 (H2 d1 u0 i H5 c2 x0 (fsubst0_both i u0 c u x0
779 H13 c2 H10)) x1 a2 (H4 d1 u0 (S i) (getl_clear_bind b (CHead c (Bind b) u) c
780 u (clear_bind b c u) (CHead d1 (Bind Abbr) u0) i H5) (CHead c2 (Bind b) x0)
781 x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t x1 H14 (CHead c2 (Bind b)
782 x0) (csubst0_both_bind b i u0 u x0 H13 c c2 H10)))) t2 H12)))))) H11))
783 (subst0_gen_head (Bind b) u0 u t t2 i H9)))) H8)) H7))))))))))))))))))))
784 (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H0: (arity g c u
785 (asucc g a1))).(\lambda (H1: ((\forall (d1: C).(\forall (u0: T).(\forall (i:
786 nat).((getl i c (CHead d1 (Bind Abbr) u0)) \to (\forall (c2: C).(\forall (t2:
787 T).((fsubst0 i u0 c u c2 t2) \to (arity g c2 t2 (asucc g
788 a1))))))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c
789 (Bind Abst) u) t a2)).(\lambda (H3: ((\forall (d1: C).(\forall (u0:
790 T).(\forall (i: nat).((getl i (CHead c (Bind Abst) u) (CHead d1 (Bind Abbr)
791 u0)) \to (\forall (c2: C).(\forall (t2: T).((fsubst0 i u0 (CHead c (Bind
792 Abst) u) t c2 t2) \to (arity g c2 t2 a2)))))))))).(\lambda (d1: C).(\lambda
793 (u0: T).(\lambda (i: nat).(\lambda (H4: (getl i c (CHead d1 (Bind Abbr)
794 u0))).(\lambda (c2: C).(\lambda (t2: T).(\lambda (H5: (fsubst0 i u0 c (THead
795 (Bind Abst) u t) c2 t2)).(let H6 \def (fsubst0_gen_base c c2 (THead (Bind
796 Abst) u t) t2 u0 i H5) in (or3_ind (land (eq C c c2) (subst0 i u0 (THead
797 (Bind Abst) u t) t2)) (land (eq T (THead (Bind Abst) u t) t2) (csubst0 i u0 c
798 c2)) (land (subst0 i u0 (THead (Bind Abst) u t) t2) (csubst0 i u0 c c2))
799 (arity g c2 t2 (AHead a1 a2)) (\lambda (H7: (land (eq C c c2) (subst0 i u0
800 (THead (Bind Abst) u t) t2))).(and_ind (eq C c c2) (subst0 i u0 (THead (Bind
801 Abst) u t) t2) (arity g c2 t2 (AHead a1 a2)) (\lambda (H8: (eq C c
802 c2)).(\lambda (H9: (subst0 i u0 (THead (Bind Abst) u t) t2)).(eq_ind C c
803 (\lambda (c0: C).(arity g c0 t2 (AHead a1 a2))) (or3_ind (ex2 T (\lambda (u2:
804 T).(eq T t2 (THead (Bind Abst) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2)))
805 (ex2 T (\lambda (t3: T).(eq T t2 (THead (Bind Abst) u t3))) (\lambda (t3:
806 T).(subst0 (s (Bind Abst) i) u0 t t3))) (ex3_2 T T (\lambda (u2: T).(\lambda
807 (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_:
808 T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s (Bind
809 Abst) i) u0 t t3)))) (arity g c t2 (AHead a1 a2)) (\lambda (H10: (ex2 T
810 (\lambda (u2: T).(eq T t2 (THead (Bind Abst) u2 t))) (\lambda (u2: T).(subst0
811 i u0 u u2)))).(ex2_ind T (\lambda (u2: T).(eq T t2 (THead (Bind Abst) u2 t)))
812 (\lambda (u2: T).(subst0 i u0 u u2)) (arity g c t2 (AHead a1 a2)) (\lambda
813 (x: T).(\lambda (H11: (eq T t2 (THead (Bind Abst) x t))).(\lambda (H12:
814 (subst0 i u0 u x)).(eq_ind_r T (THead (Bind Abst) x t) (\lambda (t0:
815 T).(arity g c t0 (AHead a1 a2))) (arity_head g c x a1 (H1 d1 u0 i H4 c x
816 (fsubst0_snd i u0 c u x H12)) t a2 (H3 d1 u0 (S i) (getl_clear_bind Abst
817 (CHead c (Bind Abst) u) c u (clear_bind Abst c u) (CHead d1 (Bind Abbr) u0) i
818 H4) (CHead c (Bind Abst) x) t (fsubst0_fst (S i) u0 (CHead c (Bind Abst) u) t
819 (CHead c (Bind Abst) x) (csubst0_snd_bind Abst i u0 u x H12 c)))) t2 H11))))
820 H10)) (\lambda (H10: (ex2 T (\lambda (t3: T).(eq T t2 (THead (Bind Abst) u
821 t3))) (\lambda (t3: T).(subst0 (s (Bind Abst) i) u0 t t3)))).(ex2_ind T
822 (\lambda (t3: T).(eq T t2 (THead (Bind Abst) u t3))) (\lambda (t3: T).(subst0
823 (s (Bind Abst) i) u0 t t3)) (arity g c t2 (AHead a1 a2)) (\lambda (x:
824 T).(\lambda (H11: (eq T t2 (THead (Bind Abst) u x))).(\lambda (H12: (subst0
825 (s (Bind Abst) i) u0 t x)).(eq_ind_r T (THead (Bind Abst) u x) (\lambda (t0:
826 T).(arity g c t0 (AHead a1 a2))) (arity_head g c u a1 H0 x a2 (H3 d1 u0 (S i)
827 (getl_clear_bind Abst (CHead c (Bind Abst) u) c u (clear_bind Abst c u)
828 (CHead d1 (Bind Abbr) u0) i H4) (CHead c (Bind Abst) u) x (fsubst0_snd (S i)
829 u0 (CHead c (Bind Abst) u) t x H12))) t2 H11)))) H10)) (\lambda (H10: (ex3_2
830 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3))))
831 (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_:
832 T).(\lambda (t3: T).(subst0 (s (Bind Abst) i) u0 t t3))))).(ex3_2_ind T T
833 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3))))
834 (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_:
835 T).(\lambda (t3: T).(subst0 (s (Bind Abst) i) u0 t t3))) (arity g c t2 (AHead
836 a1 a2)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H11: (eq T t2 (THead
837 (Bind Abst) x0 x1))).(\lambda (H12: (subst0 i u0 u x0)).(\lambda (H13:
838 (subst0 (s (Bind Abst) i) u0 t x1)).(eq_ind_r T (THead (Bind Abst) x0 x1)
839 (\lambda (t0: T).(arity g c t0 (AHead a1 a2))) (arity_head g c x0 a1 (H1 d1
840 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))).(and_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))).(and_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 H6 \def (fsubst0_gen_base c c2 (THead (Flat
914 Appl) u t) t2 u0 i H5) in (or3_ind (land (eq C c c2) (subst0 i u0 (THead
915 (Flat Appl) u t) t2)) (land (eq T (THead (Flat Appl) u t) t2) (csubst0 i u0 c
916 c2)) (land (subst0 i u0 (THead (Flat Appl) u t) t2) (csubst0 i u0 c c2))
917 (arity g c2 t2 a2) (\lambda (H7: (land (eq C c c2) (subst0 i u0 (THead (Flat
918 Appl) u t) t2))).(and_ind (eq C c c2) (subst0 i u0 (THead (Flat Appl) u t)
919 t2) (arity g c2 t2 a2) (\lambda (H8: (eq C c c2)).(\lambda (H9: (subst0 i u0
920 (THead (Flat Appl) u t) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 a2))
921 (or3_ind (ex2 T (\lambda (u2: T).(eq T t2 (THead (Flat Appl) u2 t))) (\lambda
922 (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead (Flat
923 Appl) u t3))) (\lambda (t3: T).(subst0 (s (Flat Appl) i) u0 t t3))) (ex3_2 T
924 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
925 (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_:
926 T).(\lambda (t3: T).(subst0 (s (Flat Appl) i) u0 t t3)))) (arity g c t2 a2)
927 (\lambda (H10: (ex2 T (\lambda (u2: T).(eq T t2 (THead (Flat Appl) u2 t)))
928 (\lambda (u2: T).(subst0 i u0 u u2)))).(ex2_ind T (\lambda (u2: T).(eq T t2
929 (THead (Flat Appl) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2)) (arity g c t2
930 a2) (\lambda (x: T).(\lambda (H11: (eq T t2 (THead (Flat Appl) x
931 t))).(\lambda (H12: (subst0 i u0 u x)).(eq_ind_r T (THead (Flat Appl) x t)
932 (\lambda (t0: T).(arity g c t0 a2)) (arity_appl g c x a1 (H1 d1 u0 i H4 c x
933 (fsubst0_snd i u0 c u x H12)) t a2 H2) t2 H11)))) H10)) (\lambda (H10: (ex2 T
934 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3))) (\lambda (t3: T).(subst0
935 (s (Flat Appl) i) u0 t t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead
936 (Flat Appl) u t3))) (\lambda (t3: T).(subst0 (s (Flat Appl) i) u0 t t3))
937 (arity g c t2 a2) (\lambda (x: T).(\lambda (H11: (eq T t2 (THead (Flat Appl)
938 u x))).(\lambda (H12: (subst0 (s (Flat Appl) i) u0 t x)).(eq_ind_r T (THead
939 (Flat Appl) u x) (\lambda (t0: T).(arity g c t0 a2)) (arity_appl g c u a1 H0
940 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))).(and_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))).(and_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 H6 \def (fsubst0_gen_base c c2 (THead (Flat
1009 Cast) u t) t2 u0 i H5) in (or3_ind (land (eq C c c2) (subst0 i u0 (THead
1010 (Flat Cast) u t) t2)) (land (eq T (THead (Flat Cast) u t) t2) (csubst0 i u0 c
1011 c2)) (land (subst0 i u0 (THead (Flat Cast) u t) t2) (csubst0 i u0 c c2))
1012 (arity g c2 t2 a0) (\lambda (H7: (land (eq C c c2) (subst0 i u0 (THead (Flat
1013 Cast) u t) t2))).(and_ind (eq C c c2) (subst0 i u0 (THead (Flat Cast) u t)
1014 t2) (arity g c2 t2 a0) (\lambda (H8: (eq C c c2)).(\lambda (H9: (subst0 i u0
1015 (THead (Flat Cast) u t) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 a0))
1016 (or3_ind (ex2 T (\lambda (u2: T).(eq T t2 (THead (Flat Cast) u2 t))) (\lambda
1017 (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead (Flat
1018 Cast) u t3))) (\lambda (t3: T).(subst0 (s (Flat Cast) i) u0 t t3))) (ex3_2 T
1019 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3))))
1020 (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_:
1021 T).(\lambda (t3: T).(subst0 (s (Flat Cast) i) u0 t t3)))) (arity g c t2 a0)
1022 (\lambda (H10: (ex2 T (\lambda (u2: T).(eq T t2 (THead (Flat Cast) u2 t)))
1023 (\lambda (u2: T).(subst0 i u0 u u2)))).(ex2_ind T (\lambda (u2: T).(eq T t2
1024 (THead (Flat Cast) u2 t))) (\lambda (u2: T).(subst0 i u0 u u2)) (arity g c t2
1025 a0) (\lambda (x: T).(\lambda (H11: (eq T t2 (THead (Flat Cast) x
1026 t))).(\lambda (H12: (subst0 i u0 u x)).(eq_ind_r T (THead (Flat Cast) x t)
1027 (\lambda (t0: T).(arity g c t0 a0)) (arity_cast g c x a0 (H1 d1 u0 i H4 c x
1028 (fsubst0_snd i u0 c u x H12)) t H2) t2 H11)))) H10)) (\lambda (H10: (ex2 T
1029 (\lambda (t3: T).(eq T t2 (THead (Flat Cast) u t3))) (\lambda (t3: T).(subst0
1030 (s (Flat Cast) i) u0 t t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead
1031 (Flat Cast) u t3))) (\lambda (t3: T).(subst0 (s (Flat Cast) i) u0 t t3))
1032 (arity g c t2 a0) (\lambda (x: T).(\lambda (H11: (eq T t2 (THead (Flat Cast)
1033 u x))).(\lambda (H12: (subst0 (s (Flat Cast) i) u0 t x)).(eq_ind_r T (THead
1034 (Flat Cast) u x) (\lambda (t0: T).(arity g c t0 a0)) (arity_cast g c u a0 H0
1035 x (H3 d1 u0 i H4 c x (fsubst0_snd i u0 c t x H12))) t2 H11)))) H10)) (\lambda
1036 (H10: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat
1037 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))).(and_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))).(and_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: T).(\lambda
1093 (a1: A).(\lambda (_: (arity g c t a1)).(\lambda (H1: ((\forall (d1:
1094 C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead d1 (Bind Abbr) u)) \to
1095 (\forall (c2: C).(\forall (t2: T).((fsubst0 i u c t c2 t2) \to (arity g c2 t2
1096 a1)))))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (d1:
1097 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H3: (getl i c (CHead d1 (Bind
1098 Abbr) u))).(\lambda (c2: C).(\lambda (t2: T).(\lambda (H4: (fsubst0 i u c t
1099 c2 t2)).(let H5 \def (fsubst0_gen_base c c2 t t2 u i H4) in (or3_ind (land
1100 (eq C c c2) (subst0 i u t t2)) (land (eq T t t2) (csubst0 i u c c2)) (land
1101 (subst0 i u t t2) (csubst0 i u c c2)) (arity g c2 t2 a2) (\lambda (H6: (land
1102 (eq C c c2) (subst0 i u t t2))).(and_ind (eq C c c2) (subst0 i u t t2) (arity
1103 g c2 t2 a2) (\lambda (H7: (eq C c c2)).(\lambda (H8: (subst0 i u t
1104 t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 a2)) (arity_repl g c t2 a1
1105 (H1 d1 u i H3 c t2 (fsubst0_snd i u c t t2 H8)) a2 H2) c2 H7))) H6)) (\lambda
1106 (H6: (land (eq T t t2) (csubst0 i u c c2))).(and_ind (eq T t t2) (csubst0 i u
1107 c c2) (arity g c2 t2 a2) (\lambda (H7: (eq T t t2)).(\lambda (H8: (csubst0 i
1108 u c c2)).(eq_ind T t (\lambda (t0: T).(arity g c2 t0 a2)) (arity_repl g c2 t
1109 a1 (H1 d1 u i H3 c2 t (fsubst0_fst i u c t c2 H8)) a2 H2) t2 H7))) H6))
1110 (\lambda (H6: (land (subst0 i u t t2) (csubst0 i u c c2))).(and_ind (subst0 i
1111 u t t2) (csubst0 i u c c2) (arity g c2 t2 a2) (\lambda (H7: (subst0 i u t
1112 t2)).(\lambda (H8: (csubst0 i u c c2)).(arity_repl g c2 t2 a1 (H1 d1 u i H3
1113 c2 t2 (fsubst0_both i u c t t2 H7 c2 H8)) a2 H2))) H6)) H5)))))))))))))))) c1
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