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