DEFINITION getl_wf3_trans()
TYPE =
∀i:nat.∀c1:C.∀d1:C.(getl i c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl i c2 d2)
BODY =
assume i: nat
we proceed by induction on i to prove ∀c1:C.∀d1:C.(getl i c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl i c2 d2)
case O : ⇒
the thesis becomes ∀c1:C.∀d1:C.(getl O c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2)
assume c1: C
assume d1: C
suppose H: getl O c1 d1
assume g: G
assume d2: C
suppose H0: wf3 g d1 d2
(H_x)
by (getl_gen_O . . H)
we proved clear c1 d1
by (clear_wf3_trans . . previous . . H0)
ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2
case ex_intro2 : x:C H2:wf3 g c1 x H3:clear x d2 ⇒
the thesis becomes ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2
by (drop_refl .)
we proved drop O O x x
by (getl_intro . . . . previous H3)
we proved getl O x d2
by (ex_intro2 . . . . H2 previous)
ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2
we proved ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2
∀c1:C.∀d1:C.(getl O c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl O c2 d2)
case S : n:nat ⇒
the thesis becomes ∀c1:C.∀d1:C.(getl (S n) c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl (S n) c2 d2)
(H) by induction hypothesis we know ∀c1:C.∀d1:C.(getl n c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl n c2 d2)
assume c1: C
we proceed by induction on c1 to prove ∀d1:C.(getl (S n) c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl (S n) c2 d2)
case CSort : n0:nat ⇒
the thesis becomes
∀d1:C
.∀H0:getl (S n) (CSort n0) d1
.∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g (CSort n0) c2 λc2:C.getl (S n) c2 d2)
assume d1: C
suppose H0: getl (S n) (CSort n0) d1
assume g: G
assume d2: C
suppose : wf3 g d1 d2
by (getl_gen_sort . . . H0 .)
we proved ex2 C λc2:C.wf3 g (CSort n0) c2 λc2:C.getl (S n) c2 d2
∀d1:C
.∀H0:getl (S n) (CSort n0) d1
.∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g (CSort n0) c2 λc2:C.getl (S n) c2 d2)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀d1:C
.∀H1:getl (S n) (CHead c k t) d1
.∀g:G.∀d2:C.∀H2:(wf3 g d1 d2).(ex2 C λc2:C.wf3 g (CHead c k t) c2 λc2:C.getl (S n) c2 d2)
(H0) by induction hypothesis we know ∀d1:C.(getl (S n) c d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c c2 λc2:C.getl (S n) c2 d2)
assume d1: C
suppose H1: getl (S n) (CHead c k t) d1
assume g: G
assume d2: C
suppose H2: wf3 g d1 d2
by (getl_gen_S . . . . . H1)
we proved getl (r k n) c d1
assume b: B
suppose H3: getl (r (Bind b) n) c d1
(H_x)
consider H3
we proved getl (r (Bind b) n) c d1
that is equivalent to getl n c d1
by (H . . previous . . H2)
ex2 C λc2:C.wf3 g c c2 λc2:C.getl n c2 d2
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
case ex_intro2 : x:C H5:wf3 g c x H6:getl n x d2 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
(H_x0)
by (ty3_inference . . .)
or (ex T λt2:T.ty3 g c t t2) ∀t2:T.(ty3 g c t t2)→False
end of H_x0
(H7) consider H_x0
we proceed by induction on H7 to prove ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
case or_introl : H8:ex T λt2:T.ty3 g c t t2 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
we proceed by induction on H8 to prove ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
case ex_intro : x0:T H9:ty3 g c t x0 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
(h1)
by (wf3_bind . . . H5 . . H9 .)
wf3 g (CHead c (Bind b) t) (CHead x (Bind b) t)
end of h1
(h2)
consider H6
we proved getl n x d2
that is equivalent to getl (r (Bind b) n) x d2
by (getl_head . . . . previous .)
getl (S n) (CHead x (Bind b) t) d2
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
case or_intror : H8:∀t2:T.(ty3 g c t t2)→False ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
(h1)
by (wf3_void . . . H5 . H8 .)
wf3 g (CHead c (Bind b) t) (CHead x (Bind Void) (TSort O))
end of h1
(h2)
consider H6
we proved getl n x d2
that is equivalent to getl (r (Bind Void) n) x d2
by (getl_head . . . . previous .)
getl (S n) (CHead x (Bind Void) (TSort O)) d2
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
we proved ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
∀H3:getl (r (Bind b) n) c d1
.ex2 C λc2:C.wf3 g (CHead c (Bind b) t) c2 λc2:C.getl (S n) c2 d2
assume f: F
suppose H3: getl (r (Flat f) n) c d1
(H_x)
consider H3
we proved getl (r (Flat f) n) c d1
that is equivalent to getl (S n) c d1
by (H0 . previous . . H2)
ex2 C λc2:C.wf3 g c c2 λc2:C.getl (S n) c2 d2
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ex2 C λc2:C.wf3 g (CHead c (Flat f) t) c2 λc2:C.getl (S n) c2 d2
case ex_intro2 : x:C H5:wf3 g c x H6:getl (S n) x d2 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead c (Flat f) t) c2 λc2:C.getl (S n) c2 d2
by (wf3_flat . . . H5 . .)
we proved wf3 g (CHead c (Flat f) t) x
by (ex_intro2 . . . . previous H6)
ex2 C λc2:C.wf3 g (CHead c (Flat f) t) c2 λc2:C.getl (S n) c2 d2
we proved ex2 C λc2:C.wf3 g (CHead c (Flat f) t) c2 λc2:C.getl (S n) c2 d2
∀H3:getl (r (Flat f) n) c d1
.ex2 C λc2:C.wf3 g (CHead c (Flat f) t) c2 λc2:C.getl (S n) c2 d2
by (previous . previous)
we proved ex2 C λc2:C.wf3 g (CHead c k t) c2 λc2:C.getl (S n) c2 d2
∀d1:C
.∀H1:getl (S n) (CHead c k t) d1
.∀g:G.∀d2:C.∀H2:(wf3 g d1 d2).(ex2 C λc2:C.wf3 g (CHead c k t) c2 λc2:C.getl (S n) c2 d2)
we proved ∀d1:C.(getl (S n) c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl (S n) c2 d2)
∀c1:C.∀d1:C.(getl (S n) c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl (S n) c2 d2)
we proved ∀c1:C.∀d1:C.(getl i c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl i c2 d2)
we proved ∀i:nat.∀c1:C.∀d1:C.(getl i c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl i c2 d2)