DEFINITION csubv_drop_conf()
TYPE =
∀c1:C
.∀c2:C
.(csubv c1 c2)→∀e1:C.∀h:nat.(drop h O c1 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c2 e2)
BODY =
assume c1: C
assume c2: C
suppose H: csubv c1 c2
we proceed by induction on H to prove ∀e1:C.∀h:nat.(drop h O c1 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c2 e2)
case csubv_sort : n:nat ⇒
the thesis becomes
∀e1:C.∀h:nat.∀H0:(drop h O (CSort n) e1).(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CSort n) e2)
assume e1: C
assume h: nat
suppose H0: drop h O (CSort n) e1
by (drop_gen_sort . . . . H0)
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.csubv e1 e2 λe2:C.drop h O (CSort n) 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.csubv e1 e2 λe2:C.drop h O (CSort n) e2
(h1)
by (csubv_refl .)
csubv (CSort n) (CSort n)
end of h1
(h2)
by (drop_refl .)
drop O O (CSort n) (CSort n)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 C λe2:C.csubv (CSort n) e2 λe2:C.drop O O (CSort n) e2
by (eq_ind_r . . . previous . H1)
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CSort n) e2
by (eq_ind_r . . . previous . H2)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CSort n) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CSort n) e2
∀e1:C.∀h:nat.∀H0:(drop h O (CSort n) e1).(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CSort n) e2)
case csubv_void : c3:C c4:C H0:csubv c3 c4 v1:T v2:T ⇒
the thesis becomes
∀e1:C
.∀h:nat
.∀H2:drop h O (CHead c3 (Bind Void) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind Void) v2) e2
(H1) by induction hypothesis we know ∀e1:C.∀h:nat.(drop h O c3 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c4 e2)
assume e1: C
assume h: nat
suppose H2: drop h O (CHead c3 (Bind Void) v1) e1
suppose H3: drop O O (CHead c3 (Bind Void) v1) e1
by (drop_gen_refl . . H3)
we proved eq C (CHead c3 (Bind Void) v1) e1
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind Void) v2) e2
case refl_equal : ⇒
the thesis becomes
ex2
C
λe2:C.csubv (CHead c3 (Bind Void) v1) e2
λe2:C.drop O O (CHead c4 (Bind Void) v2) e2
(h1)
by (csubv_bind_same . . H0 . . .)
csubv (CHead c3 (Bind Void) v1) (CHead c4 (Bind Void) v2)
end of h1
(h2)
by (drop_refl .)
drop O O (CHead c4 (Bind Void) v2) (CHead c4 (Bind Void) v2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csubv (CHead c3 (Bind Void) v1) e2
λe2:C.drop O O (CHead c4 (Bind Void) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind Void) v2) e2
drop O O (CHead c3 (Bind Void) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind Void) v2) e2
assume h0: nat
suppose :
drop h0 O (CHead c3 (Bind Void) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop h0 O (CHead c4 (Bind Void) v2) e2
suppose H3: drop (S h0) O (CHead c3 (Bind Void) v1) e1
(H_x)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Bind Void) h0) O c3 e1
by (H1 . . previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Bind Void) h0) O c4 e2
end of H_x
(H4) consider H_x
consider H4
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Bind Void) h0) O c4 e2
that is equivalent to ex2 C λe2:C.csubv e1 e2 λe2:C.drop h0 O c4 e2
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind Void) v2) e2
case ex_intro2 : x:C H5:csubv e1 x H6:drop h0 O c4 x ⇒
the thesis becomes ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind Void) v2) e2
consider H6
we proved drop h0 O c4 x
that is equivalent to drop (r (Bind Void) h0) O c4 x
by (drop_drop . . . . previous .)
we proved drop (S h0) O (CHead c4 (Bind Void) v2) x
by (ex_intro2 . . . . H5 previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind Void) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind Void) v2) e2
∀H3:drop (S h0) O (CHead c3 (Bind Void) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind Void) v2) e2
by (previous . H2)
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind Void) v2) e2
∀e1:C
.∀h:nat
.∀H2:drop h O (CHead c3 (Bind Void) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind Void) v2) e2
case csubv_bind : c3:C c4:C H0:csubv c3 c4 b1:B H2:not (eq B b1 Void) b2:B v1:T v2:T ⇒
the thesis becomes
∀e1:C
.∀h:nat
.∀H3:drop h O (CHead c3 (Bind b1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind b2) v2) e2
(H1) by induction hypothesis we know ∀e1:C.∀h:nat.(drop h O c3 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c4 e2)
assume e1: C
assume h: nat
suppose H3: drop h O (CHead c3 (Bind b1) v1) e1
suppose H4: drop O O (CHead c3 (Bind b1) v1) e1
by (drop_gen_refl . . H4)
we proved eq C (CHead c3 (Bind b1) v1) e1
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind b2) v2) e2
case refl_equal : ⇒
the thesis becomes ex2 C λe2:C.csubv (CHead c3 (Bind b1) v1) e2 λe2:C.drop O O (CHead c4 (Bind b2) v2) e2
(h1)
by (csubv_bind . . H0 . H2 . . .)
csubv (CHead c3 (Bind b1) v1) (CHead c4 (Bind b2) v2)
end of h1
(h2)
by (drop_refl .)
drop O O (CHead c4 (Bind b2) v2) (CHead c4 (Bind b2) v2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λe2:C.csubv (CHead c3 (Bind b1) v1) e2 λe2:C.drop O O (CHead c4 (Bind b2) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind b2) v2) e2
drop O O (CHead c3 (Bind b1) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Bind b2) v2) e2
assume h0: nat
suppose :
drop h0 O (CHead c3 (Bind b1) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop h0 O (CHead c4 (Bind b2) v2) e2
suppose H4: drop (S h0) O (CHead c3 (Bind b1) v1) e1
(H_x)
by (drop_gen_drop . . . . . H4)
we proved drop (r (Bind b1) h0) O c3 e1
by (H1 . . previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Bind b1) h0) O c4 e2
end of H_x
(H5) consider H_x
consider H5
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Bind b1) h0) O c4 e2
that is equivalent to ex2 C λe2:C.csubv e1 e2 λe2:C.drop h0 O c4 e2
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind b2) v2) e2
case ex_intro2 : x:C H6:csubv e1 x H7:drop h0 O c4 x ⇒
the thesis becomes ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind b2) v2) e2
consider H7
we proved drop h0 O c4 x
that is equivalent to drop (r (Bind b2) h0) O c4 x
by (drop_drop . . . . previous .)
we proved drop (S h0) O (CHead c4 (Bind b2) v2) x
by (ex_intro2 . . . . H6 previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind b2) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind b2) v2) e2
∀H4:drop (S h0) O (CHead c3 (Bind b1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Bind b2) v2) e2
by (previous . H3)
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind b2) v2) e2
∀e1:C
.∀h:nat
.∀H3:drop h O (CHead c3 (Bind b1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Bind b2) v2) e2
case csubv_flat : c3:C c4:C H0:csubv c3 c4 f1:F f2:F v1:T v2:T ⇒
the thesis becomes
∀e1:C
.∀h:nat
.∀H2:drop h O (CHead c3 (Flat f1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Flat f2) v2) e2
(H1) by induction hypothesis we know ∀e1:C.∀h:nat.(drop h O c3 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c4 e2)
assume e1: C
assume h: nat
suppose H2: drop h O (CHead c3 (Flat f1) v1) e1
suppose H3: drop O O (CHead c3 (Flat f1) v1) e1
by (drop_gen_refl . . H3)
we proved eq C (CHead c3 (Flat f1) v1) e1
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Flat f2) v2) e2
case refl_equal : ⇒
the thesis becomes ex2 C λe2:C.csubv (CHead c3 (Flat f1) v1) e2 λe2:C.drop O O (CHead c4 (Flat f2) v2) e2
(h1)
by (csubv_flat . . H0 . . . .)
csubv (CHead c3 (Flat f1) v1) (CHead c4 (Flat f2) v2)
end of h1
(h2)
by (drop_refl .)
drop O O (CHead c4 (Flat f2) v2) (CHead c4 (Flat f2) v2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λe2:C.csubv (CHead c3 (Flat f1) v1) e2 λe2:C.drop O O (CHead c4 (Flat f2) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Flat f2) v2) e2
drop O O (CHead c3 (Flat f1) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop O O (CHead c4 (Flat f2) v2) e2
assume h0: nat
suppose :
drop h0 O (CHead c3 (Flat f1) v1) e1
→ex2 C λe2:C.csubv e1 e2 λe2:C.drop h0 O (CHead c4 (Flat f2) v2) e2
suppose H3: drop (S h0) O (CHead c3 (Flat f1) v1) e1
(H_x)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Flat f1) h0) O c3 e1
by (H1 . . previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Flat f1) h0) O c4 e2
end of H_x
(H4) consider H_x
consider H4
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (r (Flat f1) h0) O c4 e2
that is equivalent to ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O c4 e2
we proceed by induction on the previous result to prove ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Flat f2) v2) e2
case ex_intro2 : x:C H5:csubv e1 x H6:drop (S h0) O c4 x ⇒
the thesis becomes ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Flat f2) v2) e2
consider H6
we proved drop (S h0) O c4 x
that is equivalent to drop (r (Flat f2) h0) O c4 x
by (drop_drop . . . . previous .)
we proved drop (S h0) O (CHead c4 (Flat f2) v2) x
by (ex_intro2 . . . . H5 previous)
ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Flat f2) v2) e2
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Flat f2) v2) e2
∀H3:drop (S h0) O (CHead c3 (Flat f1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop (S h0) O (CHead c4 (Flat f2) v2) e2
by (previous . H2)
we proved ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Flat f2) v2) e2
∀e1:C
.∀h:nat
.∀H2:drop h O (CHead c3 (Flat f1) v1) e1
.ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O (CHead c4 (Flat f2) v2) e2
we proved ∀e1:C.∀h:nat.(drop h O c1 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c2 e2)
we proved
∀c1:C
.∀c2:C
.(csubv c1 c2)→∀e1:C.∀h:nat.(drop h O c1 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c2 e2)