DEFINITION arity_aprem()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→∀i:nat
.∀b:A
.aprem i a b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g b))
BODY =
assume g: G
assume c: C
assume t: T
assume a: A
suppose H: arity g c t a
we proceed by induction on H to prove
∀i:nat
.∀b:A
.aprem i a b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g b))
case arity_sort : c0:C n:nat ⇒
the thesis becomes
∀i:nat
.∀b:A
.∀H0:aprem i (ASort O n) b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
assume i: nat
assume b: A
suppose H0: aprem i (ASort O n) b
(H_x)
by (aprem_gen_sort . . . . H0)
False
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
∀i:nat
.∀b:A
.∀H0:aprem i (ASort O n) b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
case arity_abbr : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes
∀i0:nat
.∀b:A
.∀H3:aprem i0 a0 b
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
(H2) by induction hypothesis we know
∀i0:nat
.∀b:A
.aprem i0 a0 b
→ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 d λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
assume i0: nat
assume b: A
suppose H3: aprem i0 a0 b
(H_x)
by (H2 . . H3)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 d λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H5:drop (plus i0 x2) O x0 d H6:arity g x0 x1 (asucc g b) ⇒
the thesis becomes ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
(H_x0)
by (getl_drop_conf_rev . . . H5 . . . . H0)
ex2 C λc1:C.drop (plus i0 x2) O c1 c0 λc1:C.drop (S i) (plus i0 x2) c1 x0
end of H_x0
(H7) consider H_x0
we proceed by induction on H7 to prove ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case ex_intro2 : x:C H8:drop (plus i0 x2) O x c0 H9:drop (S i) (plus i0 x2) x x0 ⇒
the thesis becomes ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
by (arity_lift . . . . H6 . . . H9)
we proved arity g x (lift (S i) (plus i0 x2) x1) (asucc g b)
by (ex2_3_intro . . . . . . . . H8 previous)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
we proved ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
∀i0:nat
.∀b:A
.∀H3:aprem i0 a0 b
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case arity_abst : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes
∀i0:nat
.∀b:A
.∀H3:aprem i0 a0 b
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
(H2) by induction hypothesis we know
∀i0:nat
.∀b:A
.aprem i0 (asucc g a0) b
→ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 d λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
assume i0: nat
assume b: A
suppose H3: aprem i0 a0 b
(H4)
by (aprem_asucc . . . . H3)
we proved aprem i0 (asucc g a0) b
by (H2 . . previous)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 d λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
end of H4
we proceed by induction on H4 to prove ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H5:drop (plus i0 x2) O x0 d H6:arity g x0 x1 (asucc g b) ⇒
the thesis becomes ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
(H_x)
by (getl_drop_conf_rev . . . H5 . . . . H0)
ex2 C λc1:C.drop (plus i0 x2) O c1 c0 λc1:C.drop (S i) (plus i0 x2) c1 x0
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case ex_intro2 : x:C H8:drop (plus i0 x2) O x c0 H9:drop (S i) (plus i0 x2) x x0 ⇒
the thesis becomes ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
by (arity_lift . . . . H6 . . . H9)
we proved arity g x (lift (S i) (plus i0 x2) x1) (asucc g b)
by (ex2_3_intro . . . . . . . . H8 previous)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
we proved ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
∀i0:nat
.∀b:A
.∀H3:aprem i0 a0 b
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i0 j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case arity_bind : b:B :not (eq B b Abst) c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A :arity g (CHead c0 (Bind b) u) t0 a2 ⇒
the thesis becomes
∀i:nat
.∀b0:A
.∀H5:aprem i a2 b0
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
() by induction hypothesis we know
∀i:nat
.∀b0:A
.aprem i a1 b0
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0))
(H4) by induction hypothesis we know
∀i:nat
.∀b0:A
.aprem i a2 b0
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d (CHead c0 (Bind b) u)
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0))
assume i: nat
assume b0: A
suppose H5: aprem i a2 b0
(H_x)
by (H4 . . H5)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d (CHead c0 (Bind b) u)
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
case ex2_3_intro : x0:C x1:T x2:nat H7:drop (plus i x2) O x0 (CHead c0 (Bind b) u) H8:arity g x0 x1 (asucc g b0) ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
(H9)
by (plus_n_Sm . .)
we proved eq nat (S (plus i x2)) (plus i (S x2))
we proceed by induction on the previous result to prove drop (plus i (S x2)) O x0 c0
case refl_equal : ⇒
the thesis becomes drop (S (plus i x2)) O x0 c0
by (drop_S . . . . . H7)
drop (S (plus i x2)) O x0 c0
drop (plus i (S x2)) O x0 c0
end of H9
by (ex2_3_intro . . . . . . . . H9 H8)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
∀i:nat
.∀b0:A
.∀H5:aprem i a2 b0
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b0)
case arity_head : c0:C u:T a1:A H0:arity g c0 u (asucc g a1) t0:T a2:A :arity g (CHead c0 (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀i:nat
.∀b:A
.∀H4:aprem i (AHead a1 a2) b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
() by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i (asucc g a1) b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
(H3) by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i a2 b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d (CHead c0 (Bind Abst) u)
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
assume i: nat
assume b: A
suppose H4: aprem i (AHead a1 a2) b
suppose H5: aprem O (AHead a1 a2) b
(H_y)
by (aprem_gen_head_O . . . H5)
eq A b a1
end of H_y
by (drop_refl .)
we proved drop O O c0 c0
that is equivalent to drop (plus O O) O c0 c0
by (ex2_3_intro . . . . . . . . previous H0)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g a1)
by (eq_ind_r . . . previous . H_y)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
aprem O (AHead a1 a2) b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
assume i0: nat
suppose :
aprem i0 (AHead a1 a2) b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i0 j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
suppose H5: aprem (S i0) (AHead a1 a2) b
(H_y)
by (aprem_gen_head_S . . . . H5)
aprem i0 a2 b
end of H_y
(H_x)
by (H3 . . H_y)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i0 j) O d (CHead c0 (Bind Abst) u)
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i0) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H7:drop (plus i0 x2) O x0 (CHead c0 (Bind Abst) u) H8:arity g x0 x1 (asucc g b) ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i0) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
by (drop_S . . . . . H7)
we proved drop (S (plus i0 x2)) O x0 c0
that is equivalent to drop (plus (S i0) x2) O x0 c0
by (ex2_3_intro . . . . . . . . previous H8)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i0) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i0) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
∀H5:aprem (S i0) (AHead a1 a2) b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i0) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
by (previous . H4)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
∀i:nat
.∀b:A
.∀H4:aprem i (AHead a1 a2) b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case arity_appl : c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A :arity g c0 t0 (AHead a1 a2) ⇒
the thesis becomes
∀i:nat
.∀b:A
.∀H4:aprem i a2 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
() by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i a1 b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
(H3) by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i (AHead a1 a2) b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
assume i: nat
assume b: A
suppose H4: aprem i a2 b
(H5)
by (aprem_succ . . . H4 .)
we proved aprem (S i) (AHead a1 a2) b
by (H3 . . previous)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
end of H5
consider H5
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus (S i) j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
that is equivalent to
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (S (plus i j)) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
we proceed by induction on the previous result to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H6:drop (S (plus i x2)) O x0 c0 H7:arity g x0 x1 (asucc g b) ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
assume n: nat
suppose H8: drop (S (plus i x2)) O (CSort n) c0
suppose : arity g (CSort n) x1 (asucc g b)
by (drop_gen_sort . . . . H8)
we proved and3 (eq C c0 (CSort n)) (eq nat (S (plus i x2)) O) (eq nat O O)
we proceed by induction on the previous result to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case and3_intro : :eq C c0 (CSort n) H11:eq nat (S (plus i x2)) O :eq nat O O ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
(H13)
we proceed by induction on H11 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S (plus i x2) OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S (plus i x2) OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H13
consider H13
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
∀H8:drop (S (plus i x2)) O (CSort n) c0
.arity g (CSort n) x1 (asucc g b)
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
assume d: C
suppose IHd:
drop (S (plus i x2)) O d c0
→(arity g d x1 (asucc g b)
→ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b))
assume k: K
assume t1: T
suppose H8: drop (S (plus i x2)) O (CHead d k t1) c0
suppose H9: arity g (CHead d k t1) x1 (asucc g b)
by (drop_gen_drop . . . . . H8)
we proved drop (r k (plus i x2)) O d c0
assume b0: B
suppose H10: arity g (CHead d (Bind b0) t1) x1 (asucc g b)
suppose H11: drop (r (Bind b0) (plus i x2)) O d c0
by (plus_n_Sm . .)
we proved eq nat (S (plus i x2)) (plus i (S x2))
we proceed by induction on the previous result to prove drop (plus i (S x2)) O (CHead d (Bind b0) t1) c0
case refl_equal : ⇒
the thesis becomes drop (S (plus i x2)) O (CHead d (Bind b0) t1) c0
by (drop_drop . . . . H11 .)
drop (S (plus i x2)) O (CHead d (Bind b0) t1) c0
we proved drop (plus i (S x2)) O (CHead d (Bind b0) t1) c0
by (ex2_3_intro . . . . . . . . previous H10)
we proved
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
∀H10:arity g (CHead d (Bind b0) t1) x1 (asucc g b)
.∀H11:drop (r (Bind b0) (plus i x2)) O d c0
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
assume f: F
suppose H10: arity g (CHead d (Flat f) t1) x1 (asucc g b)
suppose H11: drop (r (Flat f) (plus i x2)) O d c0
(H12)
(h1)
consider H11
we proved drop (r (Flat f) (plus i x2)) O d c0
drop (S (plus i x2)) O d c0
end of h1
(h2)
by (cimp_flat_sx . . .)
we proved cimp (CHead d (Flat f) t1) d
by (arity_cimp_conf . . . . H10 . previous)
arity g d x1 (asucc g b)
end of h2
by (IHd h1 h2)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
end of H12
we proceed by induction on H12 to prove
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
case ex2_3_intro : x3:C x4:T x5:nat H13:drop (plus i x5) O x3 c0 H14:arity g x3 x4 (asucc g b) ⇒
the thesis becomes
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
by (ex2_3_intro . . . . . . . . H13 H14)
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
we proved
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
∀H10:arity g (CHead d (Flat f) t1) x1 (asucc g b)
.∀H11:drop (r (Flat f) (plus i x2)) O d c0
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
by (previous . H9 previous)
we proved
ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
∀H8:drop (S (plus i x2)) O (CHead d k t1) c0
.∀H9:arity g (CHead d k t1) x1 (asucc g b)
.ex2_3 C T nat λd0:C.λ:T.λj:nat.drop (plus i j) O d0 c0 λd0:C.λu0:T.λ:nat.arity g d0 u0 (asucc g b)
by (previous . H6 H7)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
∀i:nat
.∀b:A
.∀H4:aprem i a2 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case arity_cast : c0:C u:T a0:A :arity g c0 u (asucc g a0) t0:T :arity g c0 t0 a0 ⇒
the thesis becomes
∀i:nat
.∀b:A
.∀H4:aprem i a0 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
() by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i (asucc g a0) b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
(H3) by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i a0 b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b))
assume i: nat
assume b: A
suppose H4: aprem i a0 b
(H_x)
by (H3 . . H4)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H6:drop (plus i x2) O x0 c0 H7:arity g x0 x1 (asucc g b) ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
by (ex2_3_intro . . . . . . . . H6 H7)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
∀i:nat
.∀b:A
.∀H4:aprem i a0 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu0:T.λ:nat.arity g d u0 (asucc g b)
case arity_repl : c0:C t0:T a1:A :arity g c0 t0 a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes
∀i:nat
.∀b:A
.∀H3:aprem i a2 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
(H1) by induction hypothesis we know
∀i:nat
.∀b:A
.aprem i a1 b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b))
assume i: nat
assume b: A
suppose H3: aprem i a2 b
(H_x)
by (aprem_repl . . . H2 . . H3)
ex2 A λb1:A.leq g b1 b λb1:A.aprem i a1 b1
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
case ex_intro2 : x:A H5:leq g x b H6:aprem i a1 x ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
(H_x0)
by (H1 . . H6)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g x)
end of H_x0
(H7) consider H_x0
we proceed by induction on H7 to prove
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
case ex2_3_intro : x0:C x1:T x2:nat H8:drop (plus i x2) O x0 c0 H9:arity g x0 x1 (asucc g x) ⇒
the thesis becomes
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
by (asucc_repl . . . H5)
we proved leq g (asucc g x) (asucc g b)
by (arity_repl . . . . H9 . previous)
we proved arity g x0 x1 (asucc g b)
by (ex2_3_intro . . . . . . . . H8 previous)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
∀i:nat
.∀b:A
.∀H3:aprem i a2 b
.ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c0
λd:C.λu:T.λ:nat.arity g d u (asucc g b)
we proved
∀i:nat
.∀b:A
.aprem i a b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g b))
we proved
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→∀i:nat
.∀b:A
.aprem i a b
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus i j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g b))