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