DEFINITION wf3_ty3_conf()
TYPE =
∀g:G.∀c1:C.∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→(ty3 g c2 t1 t2)
BODY =
assume g: G
assume c1: C
assume t1: T
assume t2: T
suppose H: ty3 g c1 t1 t2
we proceed by induction on H to prove ∀c2:C.(wf3 g c1 c2)→(ty3 g c2 t1 t2)
case ty3_conv : c:C t3:T t:T H0:ty3 g c t3 t u:T t4:T H2:ty3 g c u t4 H4:pc3 c t4 t3 ⇒
the thesis becomes ∀c2:C.∀H5:(wf3 g c c2).(ty3 g c2 u t3)
(H1) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 t3 t)
(H3) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 u t4)
assume c2: C
suppose H5: wf3 g c c2
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g c t4 t
we proceed by induction on the previous result to prove ty3 g c2 u t3
case ex_intro : x:T H6:ty3 g c t4 x ⇒
the thesis becomes ty3 g c2 u t3
(h1) by (H1 . H5) we proved ty3 g c2 t3 t
(h2) by (H3 . H5) we proved ty3 g c2 u t4
(h3)
by (wf3_pc3_conf . . . . H4 . H5 . H6 . H0)
pc3 c2 t4 t3
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c2 u t3
we proved ty3 g c2 u t3
∀c2:C.∀H5:(wf3 g c c2).(ty3 g c2 u t3)
case ty3_sort : c:C m:nat ⇒
the thesis becomes ∀c2:C.(wf3 g c c2)→(ty3 g c2 (TSort m) (TSort (next g m)))
assume c2: C
suppose : wf3 g c c2
by (ty3_sort . . .)
we proved ty3 g c2 (TSort m) (TSort (next g m))
∀c2:C.(wf3 g c c2)→(ty3 g c2 (TSort m) (TSort (next g m)))
case ty3_abbr : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abbr) u) t:T H1:ty3 g d u t ⇒
the thesis becomes ∀c2:C.∀H3:(wf3 g c c2).(ty3 g c2 (TLRef n) (lift (S n) O t))
(H2) by induction hypothesis we know ∀c2:C.(wf3 g d c2)→(ty3 g c2 u t)
assume c2: C
suppose H3: wf3 g c c2
(H_x)
by (wf3_getl_conf . . . . . H0 . . H3 . H1)
ex2 C λd2:C.getl n c2 (CHead d2 (Bind Abbr) u) λd2:C.wf3 g d d2
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ty3 g c2 (TLRef n) (lift (S n) O t)
case ex_intro2 : x:C H5:getl n c2 (CHead x (Bind Abbr) u) H6:wf3 g d x ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O t)
by (H2 . H6)
we proved ty3 g x u t
by (ty3_abbr . . . . . H5 . previous)
ty3 g c2 (TLRef n) (lift (S n) O t)
we proved ty3 g c2 (TLRef n) (lift (S n) O t)
∀c2:C.∀H3:(wf3 g c c2).(ty3 g c2 (TLRef n) (lift (S n) O t))
case ty3_abst : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abst) u) t:T H1:ty3 g d u t ⇒
the thesis becomes ∀c2:C.∀H3:(wf3 g c c2).(ty3 g c2 (TLRef n) (lift (S n) O u))
(H2) by induction hypothesis we know ∀c2:C.(wf3 g d c2)→(ty3 g c2 u t)
assume c2: C
suppose H3: wf3 g c c2
(H_x)
by (wf3_getl_conf . . . . . H0 . . H3 . H1)
ex2 C λd2:C.getl n c2 (CHead d2 (Bind Abst) u) λd2:C.wf3 g d d2
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ty3 g c2 (TLRef n) (lift (S n) O u)
case ex_intro2 : x:C H5:getl n c2 (CHead x (Bind Abst) u) H6:wf3 g d x ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O u)
by (H2 . H6)
we proved ty3 g x u t
by (ty3_abst . . . . . H5 . previous)
ty3 g c2 (TLRef n) (lift (S n) O u)
we proved ty3 g c2 (TLRef n) (lift (S n) O u)
∀c2:C.∀H3:(wf3 g c c2).(ty3 g c2 (TLRef n) (lift (S n) O u))
case ty3_bind : c:C u:T t:T H0:ty3 g c u t b:B t3:T t4:T :ty3 g (CHead c (Bind b) u) t3 t4 ⇒
the thesis becomes ∀c2:C.∀H4:(wf3 g c c2).(ty3 g c2 (THead (Bind b) u t3) (THead (Bind b) u t4))
(H1) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 u t)
(H3) by induction hypothesis we know ∀c2:C.(wf3 g (CHead c (Bind b) u) c2)→(ty3 g c2 t3 t4)
assume c2: C
suppose H4: wf3 g c c2
(h1) by (H1 . H4) we proved ty3 g c2 u t
(h2)
by (wf3_bind . . . H4 . . H0 .)
we proved wf3 g (CHead c (Bind b) u) (CHead c2 (Bind b) u)
by (H3 . previous)
ty3 g (CHead c2 (Bind b) u) t3 t4
end of h2
by (ty3_bind . . . . h1 . . . h2)
we proved ty3 g c2 (THead (Bind b) u t3) (THead (Bind b) u t4)
∀c2:C.∀H4:(wf3 g c c2).(ty3 g c2 (THead (Bind b) u t3) (THead (Bind b) u t4))
case ty3_appl : c:C w:T u:T :ty3 g c w u v:T t:T :ty3 g c v (THead (Bind Abst) u t) ⇒
the thesis becomes
∀c2:C
.∀H4:wf3 g c c2
.ty3
g
c2
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t)
(H1) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 w u)
(H3) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 v (THead (Bind Abst) u t))
assume c2: C
suppose H4: wf3 g c c2
(h1) by (H1 . H4) we proved ty3 g c2 w u
(h2)
by (H3 . H4)
ty3 g c2 v (THead (Bind Abst) u t)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
c2
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t)
∀c2:C
.∀H4:wf3 g c c2
.ty3
g
c2
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u t)
case ty3_cast : c:C t3:T t4:T :ty3 g c t3 t4 t0:T :ty3 g c t4 t0 ⇒
the thesis becomes ∀c2:C.∀H4:(wf3 g c c2).(ty3 g c2 (THead (Flat Cast) t4 t3) (THead (Flat Cast) t0 t4))
(H1) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 t3 t4)
(H3) by induction hypothesis we know ∀c2:C.(wf3 g c c2)→(ty3 g c2 t4 t0)
assume c2: C
suppose H4: wf3 g c c2
(h1) by (H1 . H4) we proved ty3 g c2 t3 t4
(h2) by (H3 . H4) we proved ty3 g c2 t4 t0
by (ty3_cast . . . . h1 . h2)
we proved ty3 g c2 (THead (Flat Cast) t4 t3) (THead (Flat Cast) t0 t4)
∀c2:C.∀H4:(wf3 g c c2).(ty3 g c2 (THead (Flat Cast) t4 t3) (THead (Flat Cast) t0 t4))
we proved ∀c2:C.(wf3 g c1 c2)→(ty3 g c2 t1 t2)
we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→(ty3 g c2 t1 t2)