DEFINITION csubt_ty3()
TYPE =
∀g:G.∀c1:C.∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→∀c2:C.(csubt 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.(csubt g c1 c2)→(ty3 g c2 t1 t2)
case ty3_conv : c:C t0:T t:T :ty3 g c t0 t u:T t3:T :ty3 g c u t3 H4:pc3 c t3 t0 ⇒
the thesis becomes ∀c2:C.∀H5:(csubt g c c2).(ty3 g c2 u t0)
(H1) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 t0 t)
(H3) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 u t3)
assume c2: C
suppose H5: csubt g c c2
(h1) by (H1 . H5) we proved ty3 g c2 t0 t
(h2) by (H3 . H5) we proved ty3 g c2 u t3
(h3) by (csubt_pc3 . . . . H4 . H5) we proved pc3 c2 t3 t0
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c2 u t0
∀c2:C.∀H5:(csubt g c c2).(ty3 g c2 u t0)
case ty3_sort : c:C m:nat ⇒
the thesis becomes ∀c2:C.(csubt g c c2)→(ty3 g c2 (TSort m) (TSort (next g m)))
assume c2: C
suppose : csubt g c c2
by (ty3_sort . . .)
we proved ty3 g c2 (TSort m) (TSort (next g m))
∀c2:C.(csubt 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 :ty3 g d u t ⇒
the thesis becomes ∀c2:C.∀H3:(csubt g c c2).(ty3 g c2 (TLRef n) (lift (S n) O t))
(H2) by induction hypothesis we know ∀c2:C.(csubt g d c2)→(ty3 g c2 u t)
assume c2: C
suppose H3: csubt g c c2
(H4)
by (csubt_getl_abbr . . . . . H0 . H3)
ex2 C λd2:C.csubt g d d2 λd2:C.getl n c2 (CHead d2 (Bind Abbr) u)
end of H4
we proceed by induction on H4 to prove ty3 g c2 (TLRef n) (lift (S n) O t)
case ex_intro2 : x:C H5:csubt g d x H6:getl n c2 (CHead x (Bind Abbr) u) ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O t)
by (H2 . H5)
we proved ty3 g x u t
by (ty3_abbr . . . . . H6 . 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:(csubt 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 :ty3 g d u t ⇒
the thesis becomes ∀c2:C.∀H3:(csubt g c c2).(ty3 g c2 (TLRef n) (lift (S n) O u))
(H2) by induction hypothesis we know ∀c2:C.(csubt g d c2)→(ty3 g c2 u t)
assume c2: C
suppose H3: csubt g c c2
(H4)
by (csubt_getl_abst . . . . . H0 . H3)
or
ex2 C λd2:C.csubt g d d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) u)
ex4_2
C
T
λd2:C.λ:T.csubt g d d2
λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d u u
λd2:C.λu:T.ty3 g d2 u u
end of H4
we proceed by induction on H4 to prove ty3 g c2 (TLRef n) (lift (S n) O u)
case or_introl : H5:ex2 C λd2:C.csubt g d d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) u) ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O u)
we proceed by induction on H5 to prove ty3 g c2 (TLRef n) (lift (S n) O u)
case ex_intro2 : x:C H6:csubt g d x H7:getl n c2 (CHead x (Bind Abst) u) ⇒
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 . . . . . H7 . previous)
ty3 g c2 (TLRef n) (lift (S n) O u)
ty3 g c2 (TLRef n) (lift (S n) O u)
case or_intror : H5:ex4_2 C T λd2:C.λ:T.csubt g d d2 λd2:C.λu0:T.getl n c2 (CHead d2 (Bind Abbr) u0) λ:C.λu0:T.ty3 g d u0 u λd2:C.λu0:T.ty3 g d2 u0 u ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O u)
we proceed by induction on H5 to prove ty3 g c2 (TLRef n) (lift (S n) O u)
case ex4_2_intro : x0:C x1:T :csubt g d x0 H7:getl n c2 (CHead x0 (Bind Abbr) x1) :ty3 g d x1 u H9:ty3 g x0 x1 u ⇒
the thesis becomes ty3 g c2 (TLRef n) (lift (S n) O u)
by (ty3_abbr . . . . . H7 . H9)
ty3 g c2 (TLRef n) (lift (S n) O u)
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:(csubt g c c2).(ty3 g c2 (TLRef n) (lift (S n) O u))
case ty3_bind : c:C u:T t:T :ty3 g c u t b:B t0:T t3:T :ty3 g (CHead c (Bind b) u) t0 t3 ⇒
the thesis becomes ∀c2:C.∀H4:(csubt g c c2).(ty3 g c2 (THead (Bind b) u t0) (THead (Bind b) u t3))
(H1) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 u t)
(H3) by induction hypothesis we know ∀c2:C.(csubt g (CHead c (Bind b) u) c2)→(ty3 g c2 t0 t3)
assume c2: C
suppose H4: csubt g c c2
(h1) by (H1 . H4) we proved ty3 g c2 u t
(h2)
by (csubt_head . . . H4 . .)
we proved csubt g (CHead c (Bind b) u) (CHead c2 (Bind b) u)
by (H3 . previous)
ty3 g (CHead c2 (Bind b) u) t0 t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
we proved ty3 g c2 (THead (Bind b) u t0) (THead (Bind b) u t3)
∀c2:C.∀H4:(csubt g c c2).(ty3 g c2 (THead (Bind b) u t0) (THead (Bind b) u t3))
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:csubt 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.(csubt g c c2)→(ty3 g c2 w u)
(H3) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 v (THead (Bind Abst) u t))
assume c2: C
suppose H4: csubt 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:csubt 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 t0:T t3:T :ty3 g c t0 t3 t4:T :ty3 g c t3 t4 ⇒
the thesis becomes ∀c2:C.∀H4:(csubt g c c2).(ty3 g c2 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t4 t3))
(H1) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 t0 t3)
(H3) by induction hypothesis we know ∀c2:C.(csubt g c c2)→(ty3 g c2 t3 t4)
assume c2: C
suppose H4: csubt g c c2
(h1) by (H1 . H4) we proved ty3 g c2 t0 t3
(h2) by (H3 . H4) we proved ty3 g c2 t3 t4
by (ty3_cast . . . . h1 . h2)
we proved ty3 g c2 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t4 t3)
∀c2:C.∀H4:(csubt g c c2).(ty3 g c2 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t4 t3))
we proved ∀c2:C.(csubt 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.(csubt g c1 c2)→(ty3 g c2 t1 t2)