1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/aprem".
19 include "arity/props.ma".
21 include "arity/cimp.ma".
23 include "aprem/props.ma".
26 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
27 a) \to (\forall (i: nat).(\forall (b: A).((aprem i a b) \to (ex2_3 C T nat
28 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c))))
29 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
32 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
33 (arity g c t a)).(arity_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda (a0:
34 A).(\forall (i: nat).(\forall (b: A).((aprem i a0 b) \to (ex2_3 C T nat
35 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
36 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
37 b)))))))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (i: nat).(\lambda
38 (b: A).(\lambda (H0: (aprem i (ASort O n) b)).(let H1 \def (match H0 in aprem
39 return (\lambda (n0: nat).(\lambda (a0: A).(\lambda (a1: A).(\lambda (_:
40 (aprem n0 a0 a1)).((eq nat n0 i) \to ((eq A a0 (ASort O n)) \to ((eq A a1 b)
41 \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
42 (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
43 nat).(arity g d u (asucc g b))))))))))))) with [(aprem_zero a1 a2)
44 \Rightarrow (\lambda (H1: (eq nat O i)).(\lambda (H2: (eq A (AHead a1 a2)
45 (ASort O n))).(\lambda (H3: (eq A a1 b)).(eq_ind nat O (\lambda (n0:
46 nat).((eq A (AHead a1 a2) (ASort O n)) \to ((eq A a1 b) \to (ex2_3 C T nat
47 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus n0 j) O d
48 c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc
49 g b))))))))) (\lambda (H4: (eq A (AHead a1 a2) (ASort O n))).(let H5 \def
50 (eq_ind A (AHead a1 a2) (\lambda (e: A).(match e in A return (\lambda (_:
51 A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
52 True])) I (ASort O n) H4) in (False_ind ((eq A a1 b) \to (ex2_3 C T nat
53 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
54 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
55 b))))))) H5))) i H1 H2 H3)))) | (aprem_succ a2 a0 i0 H1 a1) \Rightarrow
56 (\lambda (H2: (eq nat (S i0) i)).(\lambda (H3: (eq A (AHead a1 a2) (ASort O
57 n))).(\lambda (H4: (eq A a0 b)).(eq_ind nat (S i0) (\lambda (n0: nat).((eq A
58 (AHead a1 a2) (ASort O n)) \to ((eq A a0 b) \to ((aprem i0 a2 a0) \to (ex2_3
59 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus n0 j) O
60 d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u
61 (asucc g b)))))))))) (\lambda (H5: (eq A (AHead a1 a2) (ASort O n))).(let H6
62 \def (eq_ind A (AHead a1 a2) (\lambda (e: A).(match e in A return (\lambda
63 (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
64 True])) I (ASort O n) H5) in (False_ind ((eq A a0 b) \to ((aprem i0 a2 a0)
65 \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
66 (plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
67 nat).(arity g d u (asucc g b)))))))) H6))) i H2 H3 H4 H1))))]) in (H1
68 (refl_equal nat i) (refl_equal A (ASort O n)) (refl_equal A b))))))))
69 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
70 (H0: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_:
71 (arity g d u a0)).(\lambda (H2: ((\forall (i0: nat).(\forall (b: A).((aprem
72 i0 a0 b) \to (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
73 nat).(drop (plus i0 j) O d0 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
74 (_: nat).(arity g d0 u0 (asucc g b))))))))))).(\lambda (i0: nat).(\lambda (b:
75 A).(\lambda (H3: (aprem i0 a0 b)).(let H_x \def (H2 i0 b H3) in (let H4 \def
76 H_x in (ex2_3_ind C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
77 nat).(drop (plus i0 j) O d0 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
78 (_: nat).(arity g d0 u0 (asucc g b))))) (ex2_3 C T nat (\lambda (d0:
79 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda
80 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))))
81 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H5: (drop
82 (plus i0 x2) O x0 d)).(\lambda (H6: (arity g x0 x1 (asucc g b))).(let H_x0
83 \def (getl_drop_conf_rev (plus i0 x2) x0 d H5 Abbr c0 u i H0) in (let H7 \def
84 H_x0 in (ex2_ind C (\lambda (c1: C).(drop (plus i0 x2) O c1 c0)) (\lambda
85 (c1: C).(drop (S i) (plus i0 x2) c1 x0)) (ex2_3 C T nat (\lambda (d0:
86 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda
87 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))))
88 (\lambda (x: C).(\lambda (H8: (drop (plus i0 x2) O x c0)).(\lambda (H9: (drop
89 (S i) (plus i0 x2) x x0)).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_:
90 T).(\lambda (j: nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda
91 (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) x (lift (S i) (plus
92 i0 x2) x1) x2 H8 (arity_lift g x0 x1 (asucc g b) H6 x (S i) (plus i0 x2)
93 H9))))) H7)))))))) H4)))))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
94 (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abst)
95 u))).(\lambda (a0: A).(\lambda (_: (arity g d u (asucc g a0))).(\lambda (H2:
96 ((\forall (i0: nat).(\forall (b: A).((aprem i0 (asucc g a0) b) \to (ex2_3 C T
97 nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0
98 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
99 (asucc g b))))))))))).(\lambda (i0: nat).(\lambda (b: A).(\lambda (H3: (aprem
100 i0 a0 b)).(let H4 \def (H2 i0 b (aprem_asucc g a0 b i0 H3)) in (ex2_3_ind C T
101 nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d0
102 d)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
103 (asucc g b))))) (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
104 nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
105 (_: nat).(arity g d0 u0 (asucc g b)))))) (\lambda (x0: C).(\lambda (x1:
106 T).(\lambda (x2: nat).(\lambda (H5: (drop (plus i0 x2) O x0 d)).(\lambda (H6:
107 (arity g x0 x1 (asucc g b))).(let H_x \def (getl_drop_conf_rev (plus i0 x2)
108 x0 d H5 Abst c0 u i H0) in (let H7 \def H_x in (ex2_ind C (\lambda (c1:
109 C).(drop (plus i0 x2) O c1 c0)) (\lambda (c1: C).(drop (S i) (plus i0 x2) c1
110 x0)) (ex2_3 C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop
111 (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_:
112 nat).(arity g d0 u0 (asucc g b)))))) (\lambda (x: C).(\lambda (H8: (drop
113 (plus i0 x2) O x c0)).(\lambda (H9: (drop (S i) (plus i0 x2) x
114 x0)).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
115 nat).(drop (plus i0 j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda
116 (_: nat).(arity g d0 u0 (asucc g b))))) x (lift (S i) (plus i0 x2) x1) x2 H8
117 (arity_lift g x0 x1 (asucc g b) H6 x (S i) (plus i0 x2) H9))))) H7))))))))
118 H4))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
119 (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u
120 a1)).(\lambda (_: ((\forall (i: nat).(\forall (b0: A).((aprem i a1 b0) \to
121 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
122 i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
123 u0 (asucc g b0))))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_:
124 (arity g (CHead c0 (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (i:
125 nat).(\forall (b0: A).((aprem i a2 b0) \to (ex2_3 C T nat (\lambda (d:
126 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d (CHead c0 (Bind b)
127 u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
128 (asucc g b0))))))))))).(\lambda (i: nat).(\lambda (b0: A).(\lambda (H5:
129 (aprem i a2 b0)).(let H_x \def (H4 i b0 H5) in (let H6 \def H_x in (ex2_3_ind
130 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O
131 d (CHead c0 (Bind b) u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
132 nat).(arity g d u0 (asucc g b0))))) (ex2_3 C T nat (\lambda (d: C).(\lambda
133 (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
134 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b0)))))) (\lambda (x0:
135 C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H7: (drop (plus i x2) O x0
136 (CHead c0 (Bind b) u))).(\lambda (H8: (arity g x0 x1 (asucc g b0))).(let H9
137 \def (eq_ind nat (S (plus i x2)) (\lambda (n: nat).(drop n O x0 c0)) (drop_S
138 b x0 c0 u (plus i x2) H7) (plus i (S x2)) (plus_n_Sm i x2)) in (ex2_3_intro C
139 T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d
140 c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
141 (asucc g b0))))) x0 x1 (S x2) H9 H8))))))) H6))))))))))))))))) (\lambda (c0:
142 C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H0: (arity g c0 u (asucc g
143 a1))).(\lambda (_: ((\forall (i: nat).(\forall (b: A).((aprem i (asucc g a1)
144 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
145 (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
146 nat).(arity g d u0 (asucc g b))))))))))).(\lambda (t0: T).(\lambda (a2:
147 A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t0 a2)).(\lambda (H3:
148 ((\forall (i: nat).(\forall (b: A).((aprem i a2 b) \to (ex2_3 C T nat
149 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d (CHead
150 c0 (Bind Abst) u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
151 nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i: nat).(\lambda (b:
152 A).(\lambda (H4: (aprem i (AHead a1 a2) b)).(nat_ind (\lambda (n:
153 nat).((aprem n (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda
154 (_: T).(\lambda (j: nat).(drop (plus n j) O d c0)))) (\lambda (d: C).(\lambda
155 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))) (\lambda (H5:
156 (aprem O (AHead a1 a2) b)).(let H6 \def (match H5 in aprem return (\lambda
157 (n: nat).(\lambda (a0: A).(\lambda (a3: A).(\lambda (_: (aprem n a0 a3)).((eq
158 nat n O) \to ((eq A a0 (AHead a1 a2)) \to ((eq A a3 b) \to (ex2_3 C T nat
159 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
160 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
161 b))))))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (_: (eq nat O
162 O)).(\lambda (H7: (eq A (AHead a0 a3) (AHead a1 a2))).(\lambda (H8: (eq A a0
163 b)).((let H9 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda
164 (_: A).A) with [(ASort _ _) \Rightarrow a3 | (AHead _ a4) \Rightarrow a4]))
165 (AHead a0 a3) (AHead a1 a2) H7) in ((let H10 \def (f_equal A A (\lambda (e:
166 A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a0 |
167 (AHead a4 _) \Rightarrow a4])) (AHead a0 a3) (AHead a1 a2) H7) in (eq_ind A
168 a1 (\lambda (a4: A).((eq A a3 a2) \to ((eq A a4 b) \to (ex2_3 C T nat
169 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0))))
170 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
171 b))))))))) (\lambda (H11: (eq A a3 a2)).(eq_ind A a2 (\lambda (_: A).((eq A
172 a1 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
173 nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
174 (_: nat).(arity g d u0 (asucc g b)))))))) (\lambda (H12: (eq A a1 b)).(eq_ind
175 A b (\lambda (_: A).(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
176 (j: nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0:
177 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))) (eq_ind A a1 (\lambda
178 (a4: A).(ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
179 nat).(drop (plus O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
180 (_: nat).(arity g d u0 (asucc g a4))))))) (ex2_3_intro C T nat (\lambda (d:
181 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus O j) O d c0)))) (\lambda (d:
182 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g a1))))) c0 u O
183 (drop_refl c0) H0) b H12) a1 (sym_eq A a1 b H12))) a3 (sym_eq A a3 a2 H11)))
184 a0 (sym_eq A a0 a1 H10))) H9)) H8)))) | (aprem_succ a0 a3 i0 H6 a4)
185 \Rightarrow (\lambda (H7: (eq nat (S i0) O)).(\lambda (H8: (eq A (AHead a4
186 a0) (AHead a1 a2))).(\lambda (H9: (eq A a3 b)).((let H10 \def (eq_ind nat (S
187 i0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
188 \Rightarrow False | (S _) \Rightarrow True])) I O H7) in (False_ind ((eq A
189 (AHead a4 a0) (AHead a1 a2)) \to ((eq A a3 b) \to ((aprem i0 a0 a3) \to
190 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
191 O j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d
192 u0 (asucc g b))))))))) H10)) H8 H9 H6))))]) in (H6 (refl_equal nat O)
193 (refl_equal A (AHead a1 a2)) (refl_equal A b)))) (\lambda (i0: nat).(\lambda
194 (_: (((aprem i0 (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda
195 (_: T).(\lambda (j: nat).(drop (plus i0 j) O d c0)))) (\lambda (d:
196 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
197 b))))))))).(\lambda (H5: (aprem (S i0) (AHead a1 a2) b)).(let H6 \def (match
198 H5 in aprem return (\lambda (n: nat).(\lambda (a0: A).(\lambda (a3:
199 A).(\lambda (_: (aprem n a0 a3)).((eq nat n (S i0)) \to ((eq A a0 (AHead a1
200 a2)) \to ((eq A a3 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
201 T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d:
202 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))))))))
203 with [(aprem_zero a0 a3) \Rightarrow (\lambda (H6: (eq nat O (S
204 i0))).(\lambda (H7: (eq A (AHead a0 a3) (AHead a1 a2))).(\lambda (H8: (eq A
205 a0 b)).((let H9 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return
206 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
207 I (S i0) H6) in (False_ind ((eq A (AHead a0 a3) (AHead a1 a2)) \to ((eq A a0
208 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
209 (plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
210 nat).(arity g d u0 (asucc g b)))))))) H9)) H7 H8)))) | (aprem_succ a0 a3 i1
211 H6 a4) \Rightarrow (\lambda (H7: (eq nat (S i1) (S i0))).(\lambda (H8: (eq A
212 (AHead a4 a0) (AHead a1 a2))).(\lambda (H9: (eq A a3 b)).((let H10 \def
213 (f_equal nat nat (\lambda (e: nat).(match e in nat return (\lambda (_:
214 nat).nat) with [O \Rightarrow i1 | (S n) \Rightarrow n])) (S i1) (S i0) H7)
215 in (eq_ind nat i0 (\lambda (n: nat).((eq A (AHead a4 a0) (AHead a1 a2)) \to
216 ((eq A a3 b) \to ((aprem n a0 a3) \to (ex2_3 C T nat (\lambda (d: C).(\lambda
217 (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d:
218 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))
219 (\lambda (H11: (eq A (AHead a4 a0) (AHead a1 a2))).(let H12 \def (f_equal A A
220 (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _)
221 \Rightarrow a0 | (AHead _ a5) \Rightarrow a5])) (AHead a4 a0) (AHead a1 a2)
222 H11) in ((let H13 \def (f_equal A A (\lambda (e: A).(match e in A return
223 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead a5 _)
224 \Rightarrow a5])) (AHead a4 a0) (AHead a1 a2) H11) in (eq_ind A a1 (\lambda
225 (_: A).((eq A a0 a2) \to ((eq A a3 b) \to ((aprem i0 a0 a3) \to (ex2_3 C T
226 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O
227 d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0
228 (asucc g b)))))))))) (\lambda (H14: (eq A a0 a2)).(eq_ind A a2 (\lambda (a5:
229 A).((eq A a3 b) \to ((aprem i0 a5 a3) \to (ex2_3 C T nat (\lambda (d:
230 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0))))
231 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
232 b))))))))) (\lambda (H15: (eq A a3 b)).(eq_ind A b (\lambda (a5: A).((aprem
233 i0 a2 a5) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
234 nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u0:
235 T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))))) (\lambda (H16: (aprem
236 i0 a2 b)).(let H_x \def (H3 i0 b H16) in (let H17 \def H_x in (ex2_3_ind C T
237 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i0 j) O d
238 (CHead c0 (Bind Abst) u))))) (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
239 nat).(arity g d u0 (asucc g b))))) (ex2_3 C T nat (\lambda (d: C).(\lambda
240 (_: T).(\lambda (j: nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d:
241 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))) (\lambda
242 (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H18: (drop (plus i0 x2)
243 O x0 (CHead c0 (Bind Abst) u))).(\lambda (H19: (arity g x0 x1 (asucc g
244 b))).(ex2_3_intro C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
245 nat).(drop (plus (S i0) j) O d c0)))) (\lambda (d: C).(\lambda (u0:
246 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))) x0 x1 x2 (drop_S Abst x0
247 c0 u (plus i0 x2) H18) H19)))))) H17)))) a3 (sym_eq A a3 b H15))) a0 (sym_eq
248 A a0 a2 H14))) a4 (sym_eq A a4 a1 H13))) H12))) i1 (sym_eq nat i1 i0 H10)))
249 H8 H9 H6))))]) in (H6 (refl_equal nat (S i0)) (refl_equal A (AHead a1 a2))
250 (refl_equal A b)))))) i H4))))))))))))) (\lambda (c0: C).(\lambda (u:
251 T).(\lambda (a1: A).(\lambda (_: (arity g c0 u a1)).(\lambda (_: ((\forall
252 (i: nat).(\forall (b: A).((aprem i a1 b) \to (ex2_3 C T nat (\lambda (d:
253 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d:
254 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
255 b))))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0
256 (AHead a1 a2))).(\lambda (H3: ((\forall (i: nat).(\forall (b: A).((aprem i
257 (AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
258 (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
259 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i:
260 nat).(\lambda (b: A).(\lambda (H4: (aprem i a2 b)).(let H5 \def (H3 (S i) b
261 (aprem_succ a2 b i H4 a1)) in (ex2_3_ind C T nat (\lambda (d: C).(\lambda (_:
262 T).(\lambda (j: nat).(drop (S (plus i j)) O d c0)))) (\lambda (d: C).(\lambda
263 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))) (ex2_3 C T nat
264 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
265 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
266 b)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H6:
267 (drop (S (plus i x2)) O x0 c0)).(\lambda (H7: (arity g x0 x1 (asucc g
268 b))).(C_ind (\lambda (c1: C).((drop (S (plus i x2)) O c1 c0) \to ((arity g c1
269 x1 (asucc g b)) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
270 (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
271 T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))) (\lambda (n:
272 nat).(\lambda (H8: (drop (S (plus i x2)) O (CSort n) c0)).(\lambda (_: (arity
273 g (CSort n) x1 (asucc g b))).(and3_ind (eq C c0 (CSort n)) (eq nat (S (plus i
274 x2)) O) (eq nat O O) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
275 (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
276 T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))) (\lambda (_: (eq C c0
277 (CSort n))).(\lambda (H11: (eq nat (S (plus i x2)) O)).(\lambda (_: (eq nat O
278 O)).(let H13 \def (eq_ind nat (S (plus i x2)) (\lambda (ee: nat).(match ee in
279 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
280 \Rightarrow True])) I O H11) in (False_ind (ex2_3 C T nat (\lambda (d:
281 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d:
282 C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b)))))) H13)))))
283 (drop_gen_sort n (S (plus i x2)) O c0 H8))))) (\lambda (d: C).(\lambda (IHd:
284 (((drop (S (plus i x2)) O d c0) \to ((arity g d x1 (asucc g b)) \to (ex2_3 C
285 T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O
286 d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
287 (asucc g b)))))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (H8: (drop (S
288 (plus i x2)) O (CHead d k t1) c0)).(\lambda (H9: (arity g (CHead d k t1) x1
289 (asucc g b))).(K_ind (\lambda (k0: K).((arity g (CHead d k0 t1) x1 (asucc g
290 b)) \to ((drop (r k0 (plus i x2)) O d c0) \to (ex2_3 C T nat (\lambda (d0:
291 C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0 c0)))) (\lambda
292 (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b)))))))))
293 (\lambda (b0: B).(\lambda (H10: (arity g (CHead d (Bind b0) t1) x1 (asucc g
294 b))).(\lambda (H11: (drop (r (Bind b0) (plus i x2)) O d c0)).(ex2_3_intro C T
295 nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0
296 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
297 (asucc g b))))) (CHead d (Bind b0) t1) x1 (S x2) (eq_ind nat (S (plus i x2))
298 (\lambda (n: nat).(drop n O (CHead d (Bind b0) t1) c0)) (drop_drop (Bind b0)
299 (plus i x2) d c0 H11 t1) (plus i (S x2)) (plus_n_Sm i x2)) H10)))) (\lambda
300 (f: F).(\lambda (H10: (arity g (CHead d (Flat f) t1) x1 (asucc g
301 b))).(\lambda (H11: (drop (r (Flat f) (plus i x2)) O d c0)).(let H12 \def
302 (IHd H11 (arity_cimp_conf g (CHead d (Flat f) t1) x1 (asucc g b) H10 d
303 (cimp_flat_sx f d t1))) in (ex2_3_ind C T nat (\lambda (d0: C).(\lambda (_:
304 T).(\lambda (j: nat).(drop (plus i j) O d0 c0)))) (\lambda (d0: C).(\lambda
305 (u0: T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) (ex2_3 C T nat
306 (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d0
307 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
308 (asucc g b)))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5:
309 nat).(\lambda (H13: (drop (plus i x5) O x3 c0)).(\lambda (H14: (arity g x3 x4
310 (asucc g b))).(ex2_3_intro C T nat (\lambda (d0: C).(\lambda (_: T).(\lambda
311 (j: nat).(drop (plus i j) O d0 c0)))) (\lambda (d0: C).(\lambda (u0:
312 T).(\lambda (_: nat).(arity g d0 u0 (asucc g b))))) x3 x4 x5 H13 H14))))))
313 H12))))) k H9 (drop_gen_drop k d c0 t1 (plus i x2) H8)))))))) x0 H6 H7))))))
314 H5)))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a0: A).(\lambda
315 (_: (arity g c0 u (asucc g a0))).(\lambda (_: ((\forall (i: nat).(\forall (b:
316 A).((aprem i (asucc g a0) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
317 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
318 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))).(\lambda (t0:
319 T).(\lambda (_: (arity g c0 t0 a0)).(\lambda (H3: ((\forall (i: nat).(\forall
320 (b: A).((aprem i a0 b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_:
321 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
322 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i:
323 nat).(\lambda (b: A).(\lambda (H4: (aprem i a0 b)).(let H_x \def (H3 i b H4)
324 in (let H5 \def H_x in (ex2_3_ind C T nat (\lambda (d: C).(\lambda (_:
325 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda
326 (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g b))))) (ex2_3 C T nat
327 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
328 (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d u0 (asucc g
329 b)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H6:
330 (drop (plus i x2) O x0 c0)).(\lambda (H7: (arity g x0 x1 (asucc g
331 b))).(ex2_3_intro C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j:
332 nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0: T).(\lambda
333 (_: nat).(arity g d u0 (asucc g b))))) x0 x1 x2 H6 H7)))))) H5))))))))))))))
334 (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_: (arity g c0
335 t0 a1)).(\lambda (H1: ((\forall (i: nat).(\forall (b: A).((aprem i a1 b) \to
336 (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus
337 i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d
338 u (asucc g b))))))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1
339 a2)).(\lambda (i: nat).(\lambda (b: A).(\lambda (H3: (aprem i a2 b)).(let H_x
340 \def (aprem_repl g a1 a2 H2 i b H3) in (let H4 \def H_x in (ex2_ind A
341 (\lambda (b1: A).(leq g b1 b)) (\lambda (b1: A).(aprem i a1 b1)) (ex2_3 C T
342 nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d
343 c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc
344 g b)))))) (\lambda (x: A).(\lambda (H5: (leq g x b)).(\lambda (H6: (aprem i
345 a1 x)).(let H_x0 \def (H1 i x H6) in (let H7 \def H_x0 in (ex2_3_ind C T nat
346 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c0))))
347 (\lambda (d: C).(\lambda (u: T).(\lambda (_: nat).(arity g d u (asucc g
348 x))))) (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop
349 (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u: T).(\lambda (_:
350 nat).(arity g d u (asucc g b)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
351 (x2: nat).(\lambda (H8: (drop (plus i x2) O x0 c0)).(\lambda (H9: (arity g x0
352 x1 (asucc g x))).(ex2_3_intro C T nat (\lambda (d: C).(\lambda (_:
353 T).(\lambda (j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u:
354 T).(\lambda (_: nat).(arity g d u (asucc g b))))) x0 x1 x2 H8 (arity_repl g
355 x0 x1 (asucc g x) H9 (asucc g b) (asucc_repl g x b H5)))))))) H7))))))
356 H4))))))))))))) c t a H))))).