DEFINITION csuba_drop_abst_rev()
TYPE =
∀i:nat
.∀c1:C
.∀d1:C
.∀u:T
.drop i O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
BODY =
assume i: nat
we proceed by induction on i to prove
∀c1:C
.∀d1:C
.∀u:T
.drop i O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case O : ⇒
the thesis becomes
∀c1:C
.∀d1:C
.∀u:T
.drop O O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume c1: C
assume d1: C
assume u: T
suppose H: drop O O c1 (CHead d1 (Bind Abst) u)
assume g: G
assume c2: C
suppose H0: csuba g c2 c1
(H1)
by (drop_gen_refl . . H)
we proved eq C c1 (CHead d1 (Bind Abst) u)
we proceed by induction on the previous result to prove csuba g c2 (CHead d1 (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
csuba g c2 (CHead d1 (Bind Abst) u)
end of H1
(H_x)
by (csuba_gen_abst_rev . . . . H1)
or
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_introl : H3:ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H3 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H4:eq C c2 (CHead x (Bind Abst) u) H5:csuba g x d1 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (drop_refl .)
we proved drop O O (CHead x (Bind Abst) u) (CHead x (Bind Abst) u)
by (ex_intro2 . . . . previous H5)
we proved
ex2
C
λd2:C.drop O O (CHead x (Bind Abst) u) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
we proved
or
ex2
C
λd2:C.drop O O (CHead x (Bind Abst) u) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop O O (CHead x (Bind Abst) u) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_intror : H3:ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H3 to prove
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H4:eq C c2 (CHead x0 (Bind Void) x1) H5:csuba g x0 d1 ⇒
the thesis becomes
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (drop_refl .)
we proved drop O O (CHead x0 (Bind Void) x1) (CHead x0 (Bind Void) x1)
by (ex2_2_intro . . . . . . previous H5)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop O O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
we proved
or
ex2
C
λd2:C.drop O O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop O O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀c1:C
.∀d1:C
.∀u:T
.drop O O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop O O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop O O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case S : n:nat ⇒
the thesis becomes
∀c1:C
.∀d1:C
.∀u:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
(H) by induction hypothesis we know
∀c1:C
.∀d1:C
.∀u:T
.drop n O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop n O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume c1: C
we proceed by induction on c1 to prove
∀d1:C
.∀u:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case CSort : n0:nat ⇒
the thesis becomes
∀d1:C
.∀u:T
.∀H0:drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u)
.∀g:G
.∀c2:C
.csuba g c2 (CSort n0)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume d1: C
assume u: T
suppose H0: drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u)
assume g: G
assume c2: C
suppose : csuba g c2 (CSort n0)
by (drop_gen_sort . . . . H0)
we proved
and3
eq C (CHead d1 (Bind Abst) u) (CSort n0)
eq nat (S n) O
eq nat O O
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case and3_intro : :eq C (CHead d1 (Bind Abst) u) (CSort n0) H3:eq nat (S n) O :eq nat O O ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H5)
we proceed by induction on H3 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H5
consider H5
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
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀d1:C
.∀u:T
.∀H0:drop (S n) O (CSort n0) (CHead d1 (Bind Abst) u)
.∀g:G
.∀c2:C
.csuba g c2 (CSort n0)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀d1:C
.∀u:T
.∀H1:drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u)
.∀g:G
.∀c2:C
.∀H2:csuba g c2 (CHead c k t)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H0) by induction hypothesis we know
∀d1:C
.∀u:T
.drop (S n) O c (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
assume d1: C
assume u: T
suppose H1: drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u)
assume g: G
assume c2: C
suppose H2: csuba g c2 (CHead c k t)
by (drop_gen_drop . . . . . H1)
we proved drop (r k n) O c (CHead d1 (Bind Abst) u)
assume b: B
suppose H3: csuba g c2 (CHead c (Bind b) t)
suppose H4: drop (r (Bind b) n) O c (CHead d1 (Bind Abst) u)
suppose H5: csuba g c2 (CHead c (Bind Abbr) t)
suppose H6: drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u)
(H_x)
by (csuba_gen_abbr_rev . . . . H5)
or3
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abbr) t) λd2:C.csuba g d2 c
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.eq C c2 (CHead d2 (Bind Abst) u2)
λd2:C.λ:T.λ:A.csuba g d2 c
λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a)
λ:C.λ:T.λa:A.arity g c t a
ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 c
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or3_intro0 : H8:ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abbr) t) λd2:C.csuba g d2 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H9:eq C c2 (CHead x (Bind Abbr) t) H10:csuba g x c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H11)
consider H6
we proved drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H11
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H12:ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x0:C H13:drop n O x (CHead x0 (Bind Abst) u) H14:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x (CHead x0 (Bind Abst) u)
that is equivalent to drop (r (Bind Abbr) n) O x (CHead x0 (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abbr) t) (CHead x0 (Bind Abst) u)
by (ex_intro2 . . . . previous H14)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H12:ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H13:drop n O x (CHead x0 (Bind Void) x1) H14:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x (CHead x0 (Bind Void) x1)
that is equivalent to drop (r (Bind Abbr) n) O x (CHead x0 (Bind Void) x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abbr) t) (CHead x0 (Bind Void) x1)
by (ex2_2_intro . . . . . . previous H14)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or3_intro1 : H8:ex4_3 C T A λd2:C.λu2:T.λ:A.eq C c2 (CHead d2 (Bind Abst) u2) λd2:C.λ:T.λ:A.csuba g d2 c λd2:C.λu2:T.λa:A.arity g d2 u2 (asucc g a) λ:C.λ:T.λa:A.arity g c t a ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex4_3_intro : x0:C x1:T x2:A H9:eq C c2 (CHead x0 (Bind Abst) x1) H10:csuba g x0 c :arity g x0 x1 (asucc g x2) :arity g c t x2 ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H13)
consider H6
we proved drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H13
we proceed by induction on H13 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H14:ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H14 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H15:drop n O x0 (CHead x (Bind Abst) u) H16:csuba g x d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H15
we proved drop n O x0 (CHead x (Bind Abst) u)
that is equivalent to drop (r (Bind Abst) n) O x0 (CHead x (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Abst) x1) (CHead x (Bind Abst) u)
by (ex_intro2 . . . . previous H16)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H14:ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H14 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x3:C x4:T H15:drop n O x0 (CHead x3 (Bind Void) x4) H16:csuba g x3 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H15
we proved drop n O x0 (CHead x3 (Bind Void) x4)
that is equivalent to drop (r (Bind Abst) n) O x0 (CHead x3 (Bind Void) x4)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Abst) x1) (CHead x3 (Bind Void) x4)
by (ex2_2_intro . . . . . . previous H16)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or3_intro2 : H8:ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H9:eq C c2 (CHead x0 (Bind Void) x1) H10:csuba g x0 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H11)
consider H6
we proved drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H11
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H12:ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H13:drop n O x0 (CHead x (Bind Abst) u) H14:csuba g x d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x0 (CHead x (Bind Abst) u)
that is equivalent to drop (r (Bind Void) n) O x0 (CHead x (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Void) x1) (CHead x (Bind Abst) u)
by (ex_intro2 . . . . previous H14)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H12:ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x2:C x3:T H13:drop n O x0 (CHead x2 (Bind Void) x3) H14:csuba g x2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x0 (CHead x2 (Bind Void) x3)
that is equivalent to drop (r (Bind Void) n) O x0 (CHead x2 (Bind Void) x3)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Void) x1) (CHead x2 (Bind Void) x3)
by (ex2_2_intro . . . . . . previous H14)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
csuba g c2 (CHead c (Bind Abbr) t)
→(drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
suppose H5: csuba g c2 (CHead c (Bind Abst) t)
suppose H6: drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u)
(H_x)
by (csuba_gen_abst_rev . . . . H5)
or
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) t) λd2:C.csuba g d2 c
ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 c
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_introl : H8:ex2 C λd2:C.eq C c2 (CHead d2 (Bind Abst) t) λd2:C.csuba g d2 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H9:eq C c2 (CHead x (Bind Abst) t) H10:csuba g x c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H11)
consider H6
we proved drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H11
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H12:ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x0:C H13:drop n O x (CHead x0 (Bind Abst) u) H14:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x (CHead x0 (Bind Abst) u)
that is equivalent to drop (r (Bind Abst) n) O x (CHead x0 (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abst) t) (CHead x0 (Bind Abst) u)
by (ex_intro2 . . . . previous H14)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H12:ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H13:drop n O x (CHead x0 (Bind Void) x1) H14:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x (CHead x0 (Bind Void) x1)
that is equivalent to drop (r (Bind Abst) n) O x (CHead x0 (Bind Void) x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Abst) t) (CHead x0 (Bind Void) x1)
by (ex2_2_intro . . . . . . previous H14)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case or_intror : H8:ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H8 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H9:eq C c2 (CHead x0 (Bind Void) x1) H10:csuba g x0 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H11)
consider H6
we proved drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H10)
or
ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H11
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H12:ex2 C λd2:C.drop n O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H13:drop n O x0 (CHead x (Bind Abst) u) H14:csuba g x d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x0 (CHead x (Bind Abst) u)
that is equivalent to drop (r (Bind Void) n) O x0 (CHead x (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Void) x1) (CHead x (Bind Abst) u)
by (ex_intro2 . . . . previous H14)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H12:ex2_2 C T λd2:C.λu2:T.drop n O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H12 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x2:C x3:T H13:drop n O x0 (CHead x2 (Bind Void) x3) H14:csuba g x2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H13
we proved drop n O x0 (CHead x2 (Bind Void) x3)
that is equivalent to drop (r (Bind Void) n) O x0 (CHead x2 (Bind Void) x3)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Void) x1) (CHead x2 (Bind Void) x3)
by (ex2_2_intro . . . . . . previous H14)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H9)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
csuba g c2 (CHead c (Bind Abst) t)
→(drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
suppose H5: csuba g c2 (CHead c (Bind Void) t)
suppose H6: drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u)
(H_x)
by (csuba_gen_void_rev . . . . H5)
ex2 C λd2:C.eq C c2 (CHead d2 (Bind Void) t) λd2:C.csuba g d2 c
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H8:eq C c2 (CHead x (Bind Void) t) H9:csuba g x c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H10)
consider H6
we proved drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop n O c (CHead d1 (Bind Abst) u)
by (H . . . previous . . H9)
or
ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H10
we proceed by induction on H10 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H11:ex2 C λd2:C.drop n O x (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x0:C H12:drop n O x (CHead x0 (Bind Abst) u) H13:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H12
we proved drop n O x (CHead x0 (Bind Abst) u)
that is equivalent to drop (r (Bind Void) n) O x (CHead x0 (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Void) t) (CHead x0 (Bind Abst) u)
by (ex_intro2 . . . . previous H13)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H11:ex2_2 C T λd2:C.λu2:T.drop n O x (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H11 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H12:drop n O x (CHead x0 (Bind Void) x1) H13:csuba g x0 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H12
we proved drop n O x (CHead x0 (Bind Void) x1)
that is equivalent to drop (r (Bind Void) n) O x (CHead x0 (Bind Void) x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x (Bind Void) t) (CHead x0 (Bind Void) x1)
by (ex2_2_intro . . . . . . previous H13)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H8)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
csuba g c2 (CHead c (Bind Void) t)
→(drop (r (Bind Void) n) O c (CHead d1 (Bind Abst) u)
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1))
by (previous . H3 H4)
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀H3:csuba g c2 (CHead c (Bind b) t)
.∀H4:drop (r (Bind b) n) O c (CHead d1 (Bind Abst) u)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
assume f: F
suppose H3: csuba g c2 (CHead c (Flat f) t)
suppose H4: drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u)
(H_x)
by (csuba_gen_flat_rev . . . . . H3)
ex2_2 C T λd2:C.λu2:T.eq C c2 (CHead d2 (Flat f) u2) λd2:C.λ:T.csuba g d2 c
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x0:C x1:T H6:eq C c2 (CHead x0 (Flat f) x1) H7:csuba g x0 c ⇒
the thesis becomes
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
(H8)
consider H4
we proved drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u)
that is equivalent to drop (S n) O c (CHead d1 (Bind Abst) u)
by (H0 . . previous . . H7)
or
ex2 C λd2:C.drop (S n) O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
end of H8
we proceed by induction on H8 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_introl : H9:ex2 C λd2:C.drop (S n) O x0 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H9 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex_intro2 : x:C H10:drop (S n) O x0 (CHead x (Bind Abst) u) H11:csuba g x d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H10
we proved drop (S n) O x0 (CHead x (Bind Abst) u)
that is equivalent to drop (r (Flat f) n) O x0 (CHead x (Bind Abst) u)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Flat f) x1) (CHead x (Bind Abst) u)
by (ex_intro2 . . . . previous H11)
we proved
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
by (or_introl . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case or_intror : H9:ex2_2 C T λd2:C.λu2:T.drop (S n) O x0 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proceed by induction on H9 to prove
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
case ex2_2_intro : x2:C x3:T H10:drop (S n) O x0 (CHead x2 (Bind Void) x3) H11:csuba g x2 d1 ⇒
the thesis becomes
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
consider H10
we proved drop (S n) O x0 (CHead x2 (Bind Void) x3)
that is equivalent to drop (r (Flat f) n) O x0 (CHead x2 (Bind Void) x3)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Flat f) x1) (CHead x2 (Bind Void) x3)
by (ex2_2_intro . . . . . . previous H11)
we proved
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (or_intror . . previous)
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2
C
λd2:C.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u)
λd2:C.csuba g d2 d1
ex2_2
C
T
λd2:C.λu2:T.drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)
λd2:C.λ:T.csuba g d2 d1
by (eq_ind_r . . . previous . H6)
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀H3:csuba g c2 (CHead c (Flat f) t)
.∀H4:drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
by (previous . H2 previous)
we proved
or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
∀d1:C
.∀u:T
.∀H1:drop (S n) O (CHead c k t) (CHead d1 (Bind Abst) u)
.∀g:G
.∀c2:C
.∀H2:csuba g c2 (CHead c k t)
.or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1
we proved
∀d1:C
.∀u:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
∀c1:C
.∀d1:C
.∀u:T
.drop (S n) O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop (S n) O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop (S n) O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
we proved
∀c1:C
.∀d1:C
.∀u:T
.drop i O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
we proved
∀i:nat
.∀c1:C
.∀d1:C
.∀u:T
.drop i O c1 (CHead d1 (Bind Abst) u)
→∀g:G
.∀c2:C
.csuba g c2 c1
→(or
ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)