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