DEFINITION clear_wf3_trans()
TYPE =
∀c1:C.∀d1:C.(clear c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2)
BODY =
assume c1: C
assume d1: C
suppose H: clear c1 d1
we proceed by induction on H to prove ∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2)
case clear_bind : b:B e:C u:T ⇒
the thesis becomes
∀g:G
.∀d2:C
.∀H0:wf3 g (CHead e (Bind b) u) d2
.ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
assume g: G
assume d2: C
suppose H0: wf3 g (CHead e (Bind b) u) d2
(H_x)
by (wf3_gen_bind1 . . . . . H0)
or
ex3_2 C T λc2:C.λ:T.eq C d2 (CHead c2 (Bind b) u) λc2:C.λ:T.wf3 g e c2 λ:C.λw:T.ty3 g e u w
ex3
C
λc2:C.eq C d2 (CHead c2 (Bind Void) (TSort O))
λc2:C.wf3 g e c2
λ:C.∀w:T.(ty3 g e u w)→False
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
case or_introl : H2:ex3_2 C T λc2:C.λ:T.eq C d2 (CHead c2 (Bind b) u) λc2:C.λ:T.wf3 g e c2 λ:C.λw:T.ty3 g e u w ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
we proceed by induction on H2 to prove ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
case ex3_2_intro : x0:C x1:T H3:eq C d2 (CHead x0 (Bind b) u) H4:wf3 g e x0 H5:ty3 g e u x1 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
(h1)
by (wf3_bind . . . H4 . . H5 .)
wf3 g (CHead e (Bind b) u) (CHead x0 (Bind b) u)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead x0 (Bind b) u) (CHead x0 (Bind b) u)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 (CHead x0 (Bind b) u)
by (eq_ind_r . . . previous . H3)
ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
case or_intror : H2:ex3 C λc2:C.eq C d2 (CHead c2 (Bind Void) (TSort O)) λc2:C.wf3 g e c2 λ:C.∀w:T.(ty3 g e u w)→False ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
we proceed by induction on H2 to prove ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
case ex3_intro : x0:C H3:eq C d2 (CHead x0 (Bind Void) (TSort O)) H4:wf3 g e x0 H5:∀w:T.(ty3 g e u w)→False ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
(h1)
by (wf3_void . . . H4 . H5 .)
wf3 g (CHead e (Bind b) u) (CHead x0 (Bind Void) (TSort O))
end of h1
(h2)
by (clear_bind . . .)
clear
CHead x0 (Bind Void) (TSort O)
CHead x0 (Bind Void) (TSort O)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λc2:C.wf3 g (CHead e (Bind b) u) c2
λc2:C.clear c2 (CHead x0 (Bind Void) (TSort O))
by (eq_ind_r . . . previous . H3)
ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
we proved ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
∀g:G
.∀d2:C
.∀H0:wf3 g (CHead e (Bind b) u) d2
.ex2 C λc2:C.wf3 g (CHead e (Bind b) u) c2 λc2:C.clear c2 d2
case clear_flat : e:C c:C :clear e c f:F u:T ⇒
the thesis becomes ∀g:G.∀d2:C.∀H2:(wf3 g c d2).(ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2)
(H1) by induction hypothesis we know ∀g:G.∀d2:C.(wf3 g c d2)→(ex2 C λc2:C.wf3 g e c2 λc2:C.clear c2 d2)
assume g: G
assume d2: C
suppose H2: wf3 g c d2
(H_x)
by (H1 . . H2)
ex2 C λc2:C.wf3 g e c2 λc2:C.clear c2 d2
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2
case ex_intro2 : x:C H4:wf3 g e x H5:clear x d2 ⇒
the thesis becomes ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2
by (wf3_flat . . . H4 . .)
we proved wf3 g (CHead e (Flat f) u) x
by (ex_intro2 . . . . previous H5)
ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2
we proved ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2
∀g:G.∀d2:C.∀H2:(wf3 g c d2).(ex2 C λc2:C.wf3 g (CHead e (Flat f) u) c2 λc2:C.clear c2 d2)
we proved ∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2)
we proved ∀c1:C.∀d1:C.(clear c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2)