DEFINITION wf3_getl_conf()
TYPE =
∀b:B
.∀i:nat
.∀c1:C
.∀d1:C
.∀v:T
.getl i c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl i c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
BODY =
assume b: B
assume i: nat
we proceed by induction on i to prove
∀c1:C
.∀d1:C
.∀v:T
.getl i c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl i c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
case O : ⇒
the thesis becomes
∀c1:C
.∀d1:C
.∀v:T
.getl O c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
assume c1: C
assume d1: C
assume v: T
suppose H: getl O c1 (CHead d1 (Bind b) v)
assume g: G
assume c2: C
suppose H0: wf3 g c1 c2
assume w: T
suppose H1: ty3 g d1 v w
(H_y)
by (getl_gen_O . . H)
we proved clear c1 (CHead d1 (Bind b) v)
by (wf3_clear_conf . . previous . . H0)
wf3 g (CHead d1 (Bind b) v) c2
end of H_y
(H_x)
by (wf3_gen_bind1 . . . . . H_y)
or
ex3_2 C T λc2:C.λ:T.eq C c2 (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g d1 c2 λ:C.λw:T.ty3 g d1 v w
ex3
C
λc2:C.eq C c2 (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g d1 c2
λ:C.∀w:T.(ty3 g d1 v w)→False
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case or_introl : H3:ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b) v) λc3:C.λ:T.wf3 g d1 c3 λ:C.λw0:T.ty3 g d1 v w0 ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proceed by induction on H3 to prove ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case ex3_2_intro : x0:C x1:T H4:eq C c2 (CHead x0 (Bind b) v) H5:wf3 g d1 x0 :ty3 g d1 v x1 ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
by (getl_refl . . .)
we proved getl O (CHead x0 (Bind b) v) (CHead x0 (Bind b) v)
by (ex_intro2 . . . . previous H5)
we proved ex2 C λd2:C.getl O (CHead x0 (Bind b) v) (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
by (eq_ind_r . . . previous . H4)
ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case or_intror : H3:ex3 C λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O)) λc3:C.wf3 g d1 c3 λ:C.∀w0:T.(ty3 g d1 v w0)→False ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proceed by induction on H3 to prove ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case ex3_intro : x0:C H4:eq C c2 (CHead x0 (Bind Void) (TSort O)) :wf3 g d1 x0 H6:∀w0:T.(ty3 g d1 v w0)→False ⇒
the thesis becomes ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
(H_x0) by (H6 . H1) we proved False
(H7) consider H_x0
we proceed by induction on H7 to prove
ex2
C
λd2:C.getl O (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v)
λd2:C.wf3 g d1 d2
we proved
ex2
C
λd2:C.getl O (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v)
λd2:C.wf3 g d1 d2
by (eq_ind_r . . . previous . H4)
ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proved ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
∀c1:C
.∀d1:C
.∀v:T
.getl O c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl O c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
case S : n:nat ⇒
the thesis becomes
∀c1:C
.∀d1:C
.∀v:T
.getl (S n) c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
(H) by induction hypothesis we know
∀c1:C
.∀d1:C
.∀v:T
.getl n c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl n c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
assume c1: C
we proceed by induction on c1 to prove
∀d1:C
.∀v:T
.getl (S n) c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
case CSort : n0:nat ⇒
the thesis becomes
∀d1:C
.∀v:T
.∀H0:getl (S n) (CSort n0) (CHead d1 (Bind b) v)
.∀g:G
.∀c2:C
.wf3 g (CSort n0) c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
assume d1: C
assume v: T
suppose H0: getl (S n) (CSort n0) (CHead d1 (Bind b) v)
assume g: G
assume c2: C
suppose : wf3 g (CSort n0) c2
assume w: T
suppose : ty3 g d1 v w
by (getl_gen_sort . . . H0 .)
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
∀d1:C
.∀v:T
.∀H0:getl (S n) (CSort n0) (CHead d1 (Bind b) v)
.∀g:G
.∀c2:C
.wf3 g (CSort n0) c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀d1:C
.∀v:T
.∀H1:getl (S n) (CHead c k t) (CHead d1 (Bind b) v)
.∀g:G
.∀c2:C
.∀H2:wf3 g (CHead c k t) c2
.∀w:T.∀H3:(ty3 g d1 v w).(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
(H0) by induction hypothesis we know
∀d1:C
.∀v:T
.getl (S n) c (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
assume d1: C
assume v: T
suppose H1: getl (S n) (CHead c k t) (CHead d1 (Bind b) v)
assume g: G
assume c2: C
suppose H2: wf3 g (CHead c k t) c2
assume w: T
suppose H3: ty3 g d1 v w
by (getl_gen_S . . . . . H1)
we proved getl (r k n) c (CHead d1 (Bind b) v)
assume b0: B
suppose H4: wf3 g (CHead c (Bind b0) t) c2
suppose H5: getl (r (Bind b0) n) c (CHead d1 (Bind b) v)
(H_x)
by (wf3_gen_bind1 . . . . . H4)
or
ex3_2 C T λc2:C.λ:T.eq C c2 (CHead c2 (Bind b0) t) λc2:C.λ:T.wf3 g c c2 λ:C.λw:T.ty3 g c t w
ex3
C
λc2:C.eq C c2 (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g c c2
λ:C.∀w:T.(ty3 g c t w)→False
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case or_introl : H7:ex3_2 C T λc3:C.λ:T.eq C c2 (CHead c3 (Bind b0) t) λc3:C.λ:T.wf3 g c c3 λ:C.λw0:T.ty3 g c t w0 ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proceed by induction on H7 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case ex3_2_intro : x0:C x1:T H8:eq C c2 (CHead x0 (Bind b0) t) H9:wf3 g c x0 :ty3 g c t x1 ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
(H_x0)
consider H5
we proved getl (r (Bind b0) n) c (CHead d1 (Bind b) v)
that is equivalent to getl n c (CHead d1 (Bind b) v)
by (H . . . previous . . H9 . H3)
ex2 C λd2:C.getl n x0 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
end of H_x0
(H11) consider H_x0
we proceed by induction on H11 to prove
ex2 C λd2:C.getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case ex_intro2 : x:C H12:getl n x0 (CHead x (Bind b) v) H13:wf3 g d1 x ⇒
the thesis becomes
ex2 C λd2:C.getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
consider H12
we proved getl n x0 (CHead x (Bind b) v)
that is equivalent to getl (r (Bind b0) n) x0 (CHead x (Bind b) v)
by (getl_head . . . . previous .)
we proved getl (S n) (CHead x0 (Bind b0) t) (CHead x (Bind b) v)
by (ex_intro2 . . . . previous H13)
ex2 C λd2:C.getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proved
ex2 C λd2:C.getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
by (eq_ind_r . . . previous . H8)
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case or_intror : H7:ex3 C λc3:C.eq C c2 (CHead c3 (Bind Void) (TSort O)) λc3:C.wf3 g c c3 λ:C.∀w0:T.(ty3 g c t w0)→False ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proceed by induction on H7 to prove ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
case ex3_intro : x0:C H8:eq C c2 (CHead x0 (Bind Void) (TSort O)) H9:wf3 g c x0 :∀w0:T.(ty3 g c t w0)→False ⇒
the thesis becomes ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
(H_x0)
consider H5
we proved getl (r (Bind b0) n) c (CHead d1 (Bind b) v)
that is equivalent to getl n c (CHead d1 (Bind b) v)
by (H . . . previous . . H9 . H3)
ex2 C λd2:C.getl n x0 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
end of H_x0
(H11) consider H_x0
we proceed by induction on H11 to prove
ex2
C
λd2:C
.getl
S n
CHead x0 (Bind Void) (TSort O)
CHead d2 (Bind b) v
λd2:C.wf3 g d1 d2
case ex_intro2 : x:C H12:getl n x0 (CHead x (Bind b) v) H13:wf3 g d1 x ⇒
the thesis becomes
ex2
C
λd2:C
.getl
S n
CHead x0 (Bind Void) (TSort O)
CHead d2 (Bind b) v
λd2:C.wf3 g d1 d2
consider H12
we proved getl n x0 (CHead x (Bind b) v)
that is equivalent to getl (r (Bind Void) n) x0 (CHead x (Bind b) v)
by (getl_head . . . . previous .)
we proved
getl
S n
CHead x0 (Bind Void) (TSort O)
CHead x (Bind b) v
by (ex_intro2 . . . . previous H13)
ex2
C
λd2:C
.getl
S n
CHead x0 (Bind Void) (TSort O)
CHead d2 (Bind b) v
λd2:C.wf3 g d1 d2
we proved
ex2
C
λd2:C
.getl
S n
CHead x0 (Bind Void) (TSort O)
CHead d2 (Bind b) v
λd2:C.wf3 g d1 d2
by (eq_ind_r . . . previous . H8)
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
∀H4:wf3 g (CHead c (Bind b0) t) c2
.∀H5:getl (r (Bind b0) n) c (CHead d1 (Bind b) v)
.ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
assume f: F
suppose H4: wf3 g (CHead c (Flat f) t) c2
suppose H5: getl (r (Flat f) n) c (CHead d1 (Bind b) v)
(H_y) by (wf3_gen_flat1 . . . . . H4) we proved wf3 g c c2
consider H5
we proved getl (r (Flat f) n) c (CHead d1 (Bind b) v)
that is equivalent to getl (S n) c (CHead d1 (Bind b) v)
by (H0 . . previous . . H_y . H3)
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
∀H4:wf3 g (CHead c (Flat f) t) c2
.∀H5:getl (r (Flat f) n) c (CHead d1 (Bind b) v)
.ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
by (previous . H2 previous)
we proved ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2
∀d1:C
.∀v:T
.∀H1:getl (S n) (CHead c k t) (CHead d1 (Bind b) v)
.∀g:G
.∀c2:C
.∀H2:wf3 g (CHead c k t) c2
.∀w:T.∀H3:(ty3 g d1 v w).(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
we proved
∀d1:C
.∀v:T
.getl (S n) c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
∀c1:C
.∀d1:C
.∀v:T
.getl (S n) c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl (S n) c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
we proved
∀c1:C
.∀d1:C
.∀v:T
.getl i c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl i c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
we proved
∀b:B
.∀i:nat
.∀c1:C
.∀d1:C
.∀v:T
.getl i c1 (CHead d1 (Bind b) v)
→∀g:G
.∀c2:C
.wf3 g c1 c2
→∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl i c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)