DEFINITION drop_csubc_trans()
TYPE =
∀g:G
.∀c2:C
.∀e2:C
.∀d:nat
.∀h:nat
.(drop h d c2 e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g c2 c1)
BODY =
assume g: G
assume c2: C
we proceed by induction on c2 to prove
∀e2:C
.∀d:nat
.∀h:nat
.(drop h d c2 e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g c2 c1)
case CSort : n:nat ⇒
the thesis becomes
∀e2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) e2
.∀e1:C.∀H0:(csubc g e2 e1).(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1)
assume e2: C
assume d: nat
assume h: nat
suppose H: drop h d (CSort n) e2
assume e1: C
suppose H0: csubc g e2 e1
by (drop_gen_sort . . . . H)
we proved and3 (eq C e2 (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1
case and3_intro : H1:eq C e2 (CSort n) H2:eq nat h O H3:eq nat d O ⇒
the thesis becomes ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1
(H4)
we proceed by induction on H1 to prove csubc g (CSort n) e1
case refl_equal : ⇒
the thesis becomes the hypothesis H0
csubc g (CSort n) e1
end of H4
by (drop_refl .)
we proved drop O O e1 e1
by (ex_intro2 . . . . previous H4)
we proved ex2 C λc1:C.drop O O c1 e1 λc1:C.csubc g (CSort n) c1
by (eq_ind_r . . . previous . H3)
we proved ex2 C λc1:C.drop O d c1 e1 λc1:C.csubc g (CSort n) c1
by (eq_ind_r . . . previous . H2)
ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1
we proved ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1
∀e2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) e2
.∀e1:C.∀H0:(csubc g e2 e1).(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CSort n) c1)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀e2:C
.∀d:nat
.∀h:nat
.drop h d (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CHead c k t) c1)
(H) by induction hypothesis we know
∀e2:C
.∀d:nat
.∀h:nat
.(drop h d c e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g c c1)
assume e2: C
assume d: nat
we proceed by induction on d to prove
∀h:nat
.drop h d (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CHead c k t) c1)
case O : ⇒
the thesis becomes
∀h:nat
.drop h O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h O c1 e1 λc1:C.csubc g (CHead c k t) c1)
assume h: nat
we proceed by induction on h to prove
drop h O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h O c1 e1 λc1:C.csubc g (CHead c k t) c1)
case O : ⇒
the thesis becomes
drop O O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop O O c1 e1 λc1:C.csubc g (CHead c k t) c1)
suppose H0: drop O O (CHead c k t) e2
assume e1: C
suppose H1: csubc g e2 e1
(H2)
by (drop_gen_refl . . H0)
we proved eq C (CHead c k t) e2
by (eq_ind_r . . . H1 . previous)
csubc g (CHead c k t) e1
end of H2
by (drop_refl .)
we proved drop O O e1 e1
by (ex_intro2 . . . . previous H2)
we proved ex2 C λc1:C.drop O O c1 e1 λc1:C.csubc g (CHead c k t) c1
drop O O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop O O c1 e1 λc1:C.csubc g (CHead c k t) c1)
case S : n:nat ⇒
the thesis becomes
∀H1:drop (S n) O (CHead c k t) e2
.∀e1:C.∀H2:(csubc g e2 e1).(ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1)
() by induction hypothesis we know
drop n O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop n O c1 e1 λc1:C.csubc g (CHead c k t) c1)
suppose H1: drop (S n) O (CHead c k t) e2
assume e1: C
suppose H2: csubc g e2 e1
(H_x)
by (drop_gen_drop . . . . . H1)
we proved drop (r k n) O c e2
by (H . . . previous . H2)
ex2 C λc1:C.drop (r k n) O c1 e1 λc1:C.csubc g c c1
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1
case ex_intro2 : x:C H4:drop (r k n) O x e1 H5:csubc g c x ⇒
the thesis becomes ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1
(h1)
by (drop_drop . . . . H4 .)
drop (S n) O (CHead x k t) e1
end of h1
(h2)
by (csubc_head . . . H5 . .)
csubc g (CHead c k t) (CHead x k t)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1
we proved ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1
∀H1:drop (S n) O (CHead c k t) e2
.∀e1:C.∀H2:(csubc g e2 e1).(ex2 C λc1:C.drop (S n) O c1 e1 λc1:C.csubc g (CHead c k t) c1)
we proved
drop h O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h O c1 e1 λc1:C.csubc g (CHead c k t) c1)
∀h:nat
.drop h O (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h O c1 e1 λc1:C.csubc g (CHead c k t) c1)
case S : n:nat ⇒
the thesis becomes
∀h:nat
.∀H1:drop h (S n) (CHead c k t) e2
.∀e1:C.∀H2:(csubc g e2 e1).(ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1)
(H0) by induction hypothesis we know
∀h:nat
.drop h n (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h n c1 e1 λc1:C.csubc g (CHead c k t) c1)
assume h: nat
suppose H1: drop h (S n) (CHead c k t) e2
assume e1: C
suppose H2: csubc g e2 e1
by (drop_gen_skip_l . . . . . . H1)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e2 (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k n) v)
λe:C.λ:T.drop h (r k n) c e
we proceed by induction on the previous result to prove ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1
case ex3_2_intro : x0:C x1:T H3:eq C e2 (CHead x0 k x1) H4:eq T t (lift h (r k n) x1) H5:drop h (r k n) c x0 ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1
(H6)
we proceed by induction on H3 to prove csubc g (CHead x0 k x1) e1
case refl_equal : ⇒
the thesis becomes the hypothesis H2
csubc g (CHead x0 k x1) e1
end of H6
(H7)
we proceed by induction on H3 to prove
∀h0:nat
.drop h0 n (CHead c k t) (CHead x0 k x1)
→∀e3:C
.csubc g (CHead x0 k x1) e3
→ex2 C λc1:C.drop h0 n c1 e3 λc1:C.csubc g (CHead c k t) c1
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀h0:nat
.drop h0 n (CHead c k t) (CHead x0 k x1)
→∀e3:C
.csubc g (CHead x0 k x1) e3
→ex2 C λc1:C.drop h0 n c1 e3 λc1:C.csubc g (CHead c k t) c1
end of H7
(H8)
we proceed by induction on H4 to prove
∀h0:nat
.drop h0 n (CHead c k (lift h (r k n) x1)) (CHead x0 k x1)
→∀e3:C
.csubc g (CHead x0 k x1) e3
→ex2 C λc1:C.drop h0 n c1 e3 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
∀h0:nat
.drop h0 n (CHead c k (lift h (r k n) x1)) (CHead x0 k x1)
→∀e3:C
.csubc g (CHead x0 k x1) e3
→ex2 C λc1:C.drop h0 n c1 e3 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
end of H8
(H_x)
by (csubc_gen_head_l . . . . . H6)
or3
ex2 C λc2:C.eq C e1 (CHead c2 k x1) λc2:C.csubc g x0 c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K k (Bind Abst)
λc2:C.λw:T.λ:A.eq C e1 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g x0 c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) x0 x1
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C e1 (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 x0 c2
end of H_x
(H9) consider H_x
we proceed by induction on H9 to prove ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case or3_intro0 : H10:ex2 C λc3:C.eq C e1 (CHead c3 k x1) λc3:C.csubc g x0 c3 ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
we proceed by induction on H10 to prove ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case ex_intro2 : x:C H11:eq C e1 (CHead x k x1) H12:csubc g x0 x ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
(H_x0)
by (H . . . H5 . H12)
ex2 C λc1:C.drop h (r k n) c1 x λc1:C.csubc g c c1
end of H_x0
(H13) consider H_x0
we proceed by induction on H13 to prove
ex2
C
λc1:C.drop h (S n) c1 (CHead x k x1)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case ex_intro2 : x2:C H14:drop h (r k n) x2 x H15:csubc g c x2 ⇒
the thesis becomes
ex2
C
λc1:C.drop h (S n) c1 (CHead x k x1)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
(h1)
by (drop_skip . . . . . H14 .)
drop h (S n) (CHead x2 k (lift h (r k n) x1)) (CHead x k x1)
end of h1
(h2)
by (csubc_head . . . H15 . .)
csubc
g
CHead c k (lift h (r k n) x1)
CHead x2 k (lift h (r k n) x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λc1:C.drop h (S n) c1 (CHead x k x1)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
we proved
ex2
C
λc1:C.drop h (S n) c1 (CHead x k x1)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
by (eq_ind_r . . . previous . H11)
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case or3_intro1 : H10:ex5_3 C T A λ:C.λ:T.λ:A.eq K k (Bind Abst) λc3:C.λw:T.λ:A.eq C e1 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g x0 c3 λ:C.λ:T.λa:A.sc3 g (asucc g a) x0 x1 λc3:C.λw:T.λa:A.sc3 g a c3 w ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
we proceed by induction on H10 to prove ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case ex5_3_intro : x2:C x3:T x4:A H11:eq K k (Bind Abst) H12:eq C e1 (CHead x2 (Bind Abbr) x3) H13:csubc g x0 x2 H14:sc3 g (asucc g x4) x0 x1 H15:sc3 g x4 x2 x3 ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
(H17)
we proceed by induction on H11 to prove drop h (r (Bind Abst) n) c x0
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (r (Bind Abst) n) c x0
end of H17
(H_x0)
by (H . . . H17 . H13)
ex2 C λc1:C.drop h (r (Bind Abst) n) c1 x2 λc1:C.csubc g c c1
end of H_x0
(H18) consider H_x0
consider H18
we proved ex2 C λc1:C.drop h (r (Bind Abst) n) c1 x2 λc1:C.csubc g c c1
that is equivalent to ex2 C λc1:C.drop h n c1 x2 λc1:C.csubc g c c1
we proceed by induction on the previous result to prove
ex2
C
λc1:C.drop h (S n) c1 (CHead x2 (Bind Abbr) x3)
λc1:C.csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1
case ex_intro2 : x:C H19:drop h n x x2 H20:csubc g c x ⇒
the thesis becomes
ex2
C
λc1:C.drop h (S n) c1 (CHead x2 (Bind Abbr) x3)
λc1:C.csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1
(h1)
by (drop_skip_bind . . . . H19 . .)
drop
h
S n
CHead x (Bind Abbr) (lift h n x3)
CHead x2 (Bind Abbr) x3
end of h1
(h2)
(h1)
by (sc3_lift . . . . H14 . . . H17)
sc3 g (asucc g x4) c (lift h (r (Bind Abst) n) x1)
end of h1
(h2)
by (sc3_lift . . . . H15 . . . H19)
sc3 g x4 x (lift h n x3)
end of h2
by (csubc_abst . . . H20 . . h1 . h2)
csubc
g
CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)
CHead x (Bind Abbr) (lift h n x3)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λc1:C.drop h (S n) c1 (CHead x2 (Bind Abbr) x3)
λc1:C.csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1
we proved
ex2
C
λc1:C.drop h (S n) c1 (CHead x2 (Bind Abbr) x3)
λc1:C.csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1
by (eq_ind_r . . . previous . H11)
we proved
ex2
C
λc1:C.drop h (S n) c1 (CHead x2 (Bind Abbr) x3)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
by (eq_ind_r . . . previous . H12)
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case or3_intro2 : H10:ex4_3 B C T λb:B.λc3:C.λv2:T.eq C e1 (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 x0 c3 ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
we proceed by induction on H10 to prove ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
case ex4_3_intro : x2:B x3:C x4:T H11:eq C e1 (CHead x3 (Bind x2) x4) H12:eq K k (Bind Void) H13:not (eq B x2 Void) H14:csubc g x0 x3 ⇒
the thesis becomes ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
(H16)
we proceed by induction on H12 to prove drop h (r (Bind Void) n) c x0
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (r (Bind Void) n) c x0
end of H16
(H_x0)
by (H . . . H16 . H14)
ex2 C λc1:C.drop h (r (Bind Void) n) c1 x3 λc1:C.csubc g c c1
end of H_x0
(H17) consider H_x0
consider H17
we proved ex2 C λc1:C.drop h (r (Bind Void) n) c1 x3 λc1:C.csubc g c c1
that is equivalent to ex2 C λc1:C.drop h n c1 x3 λc1:C.csubc g c c1
we proceed by induction on the previous result to prove
ex2
C
λc1:C.drop h (S n) c1 (CHead x3 (Bind x2) x4)
λc1:C.csubc g (CHead c (Bind Void) (lift h (r (Bind Void) n) x1)) c1
case ex_intro2 : x:C H18:drop h n x x3 H19:csubc g c x ⇒
the thesis becomes
ex2
C
λc1:C.drop h (S n) c1 (CHead x3 (Bind x2) x4)
λc1:C.csubc g (CHead c (Bind Void) (lift h (r (Bind Void) n) x1)) c1
(h1)
by (drop_skip_bind . . . . H18 . .)
drop h (S n) (CHead x (Bind x2) (lift h n x4)) (CHead x3 (Bind x2) x4)
end of h1
(h2)
by (csubc_void . . . H19 . H13 . .)
csubc
g
CHead c (Bind Void) (lift h (r (Bind Void) n) x1)
CHead x (Bind x2) (lift h n x4)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λc1:C.drop h (S n) c1 (CHead x3 (Bind x2) x4)
λc1:C.csubc g (CHead c (Bind Void) (lift h (r (Bind Void) n) x1)) c1
we proved
ex2
C
λc1:C.drop h (S n) c1 (CHead x3 (Bind x2) x4)
λc1:C.csubc g (CHead c (Bind Void) (lift h (r (Bind Void) n) x1)) c1
by (eq_ind_r . . . previous . H12)
we proved
ex2
C
λc1:C.drop h (S n) c1 (CHead x3 (Bind x2) x4)
λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
by (eq_ind_r . . . previous . H11)
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
we proved ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k (lift h (r k n) x1)) c1
by (eq_ind_r . . . previous . H4)
ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1
we proved ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1
∀h:nat
.∀H1:drop h (S n) (CHead c k t) e2
.∀e1:C.∀H2:(csubc g e2 e1).(ex2 C λc1:C.drop h (S n) c1 e1 λc1:C.csubc g (CHead c k t) c1)
we proved
∀h:nat
.drop h d (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CHead c k t) c1)
∀e2:C
.∀d:nat
.∀h:nat
.drop h d (CHead c k t) e2
→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g (CHead c k t) c1)
we proved
∀e2:C
.∀d:nat
.∀h:nat
.(drop h d c2 e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g c2 c1)
we proved
∀g:G
.∀c2:C
.∀e2:C
.∀d:nat
.∀h:nat
.(drop h d c2 e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop h d c1 e1 λc1:C.csubc g c2 c1)