DEFINITION csubc_drop_conf_O()
TYPE =
∀g:G
.∀c1:C
.∀e1:C
.∀h:nat
.(drop h O c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
BODY =
assume g: G
assume c1: C
we proceed by induction on c1 to prove
∀e1:C
.∀h:nat
.(drop h O c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
case CSort : n:nat ⇒
the thesis becomes
∀e1:C
.∀h:nat
.∀H:drop h O (CSort n) e1
.∀c2:C.∀H0:(csubc g (CSort n) c2).(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
assume e1: C
assume h: nat
suppose H: drop h O (CSort n) e1
assume c2: C
suppose H0: csubc g (CSort n) c2
by (drop_gen_sort . . . . H)
we proved and3 (eq C e1 (CSort n)) (eq nat h O) (eq nat O O)
we proceed by induction on the previous result to prove ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2
case and3_intro : H1:eq C e1 (CSort n) H2:eq nat h O :eq nat O O ⇒
the thesis becomes ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2
by (drop_refl .)
we proved drop O O c2 c2
by (ex_intro2 . . . . previous H0)
we proved ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g (CSort n) e2
by (eq_ind_r . . . previous . H1)
we proved ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g e1 e2
by (eq_ind_r . . . previous . H2)
ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2
we proved ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2
∀e1:C
.∀h:nat
.∀H:drop h O (CSort n) e1
.∀c2:C.∀H0:(csubc g (CSort n) c2).(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀e1:C
.∀h:nat
.drop h O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
(H) by induction hypothesis we know
∀e1:C
.∀h:nat
.(drop h O c e1)→∀c2:C.(csubc g c c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
assume e1: C
assume h: nat
we proceed by induction on h to prove
drop h O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
case O : ⇒
the thesis becomes
drop O O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g e1 e2)
suppose H0: drop O O (CHead c k t) e1
assume c2: C
suppose H1: csubc g (CHead c k t) c2
by (drop_gen_refl . . H0)
we proved eq C (CHead c k t) e1
we proceed by induction on the previous result to prove ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g e1 e2
case refl_equal : ⇒
the thesis becomes ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g (CHead c k t) e2
by (drop_refl .)
we proved drop O O c2 c2
by (ex_intro2 . . . . previous H1)
ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g (CHead c k t) e2
we proved ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g e1 e2
drop O O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop O O c2 e2 λe2:C.csubc g e1 e2)
case S : n:nat ⇒
the thesis becomes
∀H1:drop (S n) O (CHead c k t) e1
.∀c2:C.∀H2:(csubc g (CHead c k t) c2).(ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2)
(H0) by induction hypothesis we know
drop n O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop n O c2 e2 λe2:C.csubc g e1 e2)
suppose H1: drop (S n) O (CHead c k t) e1
assume c2: C
suppose H2: csubc g (CHead c k t) c2
(H_x)
by (csubc_gen_head_l . . . . . H2)
or3
ex2 C λc2:C.eq C c2 (CHead c2 k t) λc2:C.csubc g c c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C c2 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g c c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) c t
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C c2 (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K k (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g c c2
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case or3_intro0 : H4:ex2 C λc3:C.eq C c2 (CHead c3 k t) λc3:C.csubc g c c3 ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
we proceed by induction on H4 to prove ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case ex_intro2 : x:C H5:eq C c2 (CHead x k t) H6:csubc g c x ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
(H_x0)
by (drop_gen_drop . . . . . H1)
we proved drop (r k n) O c e1
by (H . . previous . H6)
ex2 C λe2:C.drop (r k n) O x e2 λe2:C.csubc g e1 e2
end of H_x0
(H7) consider H_x0
we proceed by induction on H7 to prove ex2 C λe2:C.drop (S n) O (CHead x k t) e2 λe2:C.csubc g e1 e2
case ex_intro2 : x0:C H8:drop (r k n) O x x0 H9:csubc g e1 x0 ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O (CHead x k t) e2 λe2:C.csubc g e1 e2
by (drop_drop . . . . H8 .)
we proved drop (S n) O (CHead x k t) x0
by (ex_intro2 . . . . previous H9)
ex2 C λe2:C.drop (S n) O (CHead x k t) e2 λe2:C.csubc g e1 e2
we proved ex2 C λe2:C.drop (S n) O (CHead x k t) e2 λe2:C.csubc g e1 e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case or3_intro1 : H4:ex5_3 C T A λ:C.λ:T.λ:A.eq K k (Bind Abst) λc3:C.λw:T.λ:A.eq C c2 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g c c3 λ:C.λ:T.λa:A.sc3 g (asucc g a) c t λc3:C.λw:T.λa:A.sc3 g a c3 w ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
we proceed by induction on H4 to prove ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case ex5_3_intro : x0:C x1:T x2:A H5:eq K k (Bind Abst) H6:eq C c2 (CHead x0 (Bind Abbr) x1) H7:csubc g c x0 :sc3 g (asucc g x2) c t :sc3 g x2 x0 x1 ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
(H10)
we proceed by induction on H5 to prove drop (r (Bind Abst) n) O c e1
case refl_equal : ⇒
the thesis becomes drop (r k n) O c e1
by (drop_gen_drop . . . . . H1)
drop (r k n) O c e1
drop (r (Bind Abst) n) O c e1
end of H10
(H_x0)
by (H . . H10 . H7)
ex2 C λe2:C.drop (r (Bind Abst) n) O x0 e2 λe2:C.csubc g e1 e2
end of H_x0
(H12) consider H_x0
consider H12
we proved ex2 C λe2:C.drop (r (Bind Abst) n) O x0 e2 λe2:C.csubc g e1 e2
that is equivalent to ex2 C λe2:C.drop n O x0 e2 λe2:C.csubc g e1 e2
we proceed by induction on the previous result to prove ex2 C λe2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g e1 e2
case ex_intro2 : x:C H13:drop n O x0 x H14:csubc g e1 x ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g e1 e2
consider H13
we proved drop n O x0 x
that is equivalent to drop (r (Bind Abbr) n) O x0 x
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x0 (Bind Abbr) x1) x
by (ex_intro2 . . . . previous H14)
ex2 C λe2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g e1 e2
we proved ex2 C λe2:C.drop (S n) O (CHead x0 (Bind Abbr) x1) e2 λe2:C.csubc g e1 e2
by (eq_ind_r . . . previous . H6)
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case or3_intro2 : H4:ex4_3 B C T λb:B.λc3:C.λv2:T.eq C c2 (CHead c3 (Bind b) v2) λ:B.λ:C.λ:T.eq K k (Bind Void) λb:B.λ:C.λ:T.not (eq B b Void) λ:B.λc3:C.λ:T.csubc g c c3 ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
we proceed by induction on H4 to prove ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
case ex4_3_intro : x0:B x1:C x2:T H5:eq C c2 (CHead x1 (Bind x0) x2) H6:eq K k (Bind Void) :not (eq B x0 Void) H8:csubc g c x1 ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
(H9)
we proceed by induction on H6 to prove drop (r (Bind Void) n) O c e1
case refl_equal : ⇒
the thesis becomes drop (r k n) O c e1
by (drop_gen_drop . . . . . H1)
drop (r k n) O c e1
drop (r (Bind Void) n) O c e1
end of H9
(H_x0)
by (H . . H9 . H8)
ex2 C λe2:C.drop (r (Bind Void) n) O x1 e2 λe2:C.csubc g e1 e2
end of H_x0
(H11) consider H_x0
consider H11
we proved ex2 C λe2:C.drop (r (Bind Void) n) O x1 e2 λe2:C.csubc g e1 e2
that is equivalent to ex2 C λe2:C.drop n O x1 e2 λe2:C.csubc g e1 e2
we proceed by induction on the previous result to prove ex2 C λe2:C.drop (S n) O (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g e1 e2
case ex_intro2 : x:C H12:drop n O x1 x H13:csubc g e1 x ⇒
the thesis becomes ex2 C λe2:C.drop (S n) O (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g e1 e2
consider H12
we proved drop n O x1 x
that is equivalent to drop (r (Bind x0) n) O x1 x
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead x1 (Bind x0) x2) x
by (ex_intro2 . . . . previous H13)
ex2 C λe2:C.drop (S n) O (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g e1 e2
we proved ex2 C λe2:C.drop (S n) O (CHead x1 (Bind x0) x2) e2 λe2:C.csubc g e1 e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
we proved ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2
∀H1:drop (S n) O (CHead c k t) e1
.∀c2:C.∀H2:(csubc g (CHead c k t) c2).(ex2 C λe2:C.drop (S n) O c2 e2 λe2:C.csubc g e1 e2)
we proved
drop h O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
∀e1:C
.∀h:nat
.drop h O (CHead c k t) e1
→∀c2:C.(csubc g (CHead c k t) c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
we proved
∀e1:C
.∀h:nat
.(drop h O c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
we proved
∀g:G
.∀c1:C
.∀e1:C
.∀h:nat
.(drop h O c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)