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