DEFINITION ty3_sty0()
TYPE =
∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(sty0 g c u t2)→(ty3 g c u t2)
BODY =
assume g: G
assume c: C
assume u: T
assume t1: T
suppose H: ty3 g c u t1
we proceed by induction on H to prove ∀t2:T.(sty0 g c u t2)→(ty3 g c u t2)
case ty3_conv : c0:C t2:T t:T :ty3 g c0 t2 t u0:T t3:T :ty3 g c0 u0 t3 :pc3 c0 t3 t2 ⇒
the thesis becomes ∀t0:T.∀H5:(sty0 g c0 u0 t0).(ty3 g c0 u0 t0)
() by induction hypothesis we know ∀t3:T.(sty0 g c0 t2 t3)→(ty3 g c0 t2 t3)
(H3) by induction hypothesis we know ∀t4:T.(sty0 g c0 u0 t4)→(ty3 g c0 u0 t4)
assume t0: T
suppose H5: sty0 g c0 u0 t0
by (H3 . H5)
we proved ty3 g c0 u0 t0
∀t0:T.∀H5:(sty0 g c0 u0 t0).(ty3 g c0 u0 t0)
case ty3_sort : c0:C m:nat ⇒
the thesis becomes ∀t2:T.∀H0:(sty0 g c0 (TSort m) t2).(ty3 g c0 (TSort m) t2)
assume t2: T
suppose H0: sty0 g c0 (TSort m) t2
(H_y)
by (sty0_gen_sort . . . . H0)
eq T t2 (TSort (next g m))
end of H_y
(H1)
by (f_equal . . . . . H_y)
we proved eq T t2 (TSort (next g m))
eq T (λe:T.e t2) (λe:T.e (TSort (next g m)))
end of H1
by (ty3_sort . . .)
we proved ty3 g c0 (TSort m) (TSort (next g m))
by (eq_ind_r . . . previous . H1)
we proved ty3 g c0 (TSort m) t2
∀t2:T.∀H0:(sty0 g c0 (TSort m) t2).(ty3 g c0 (TSort m) t2)
case ty3_abbr : n:nat c0:C d:C u0:T H0:getl n c0 (CHead d (Bind Abbr) u0) t:T :ty3 g d u0 t ⇒
the thesis becomes ∀t2:T.∀H3:(sty0 g c0 (TLRef n) t2).(ty3 g c0 (TLRef n) t2)
(H2) by induction hypothesis we know ∀t2:T.(sty0 g d u0 t2)→(ty3 g d u0 t2)
assume t2: T
suppose H3: sty0 g c0 (TLRef n) t2
(H_x)
by (sty0_gen_lref . . . . H3)
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T t2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T t2 (lift (S n) O u)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ty3 g c0 (TLRef n) t2
case or_introl : H5:ex3_3 C T T λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abbr) u1) λe:C.λu1:T.λt0:T.sty0 g e u1 t0 λ:C.λ:T.λt0:T.eq T t2 (lift (S n) O t0) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
we proceed by induction on H5 to prove ty3 g c0 (TLRef n) t2
case ex3_3_intro : x0:C x1:T x2:T H6:getl n c0 (CHead x0 (Bind Abbr) x1) H7:sty0 g x0 x1 x2 H8:eq T t2 (lift (S n) O x2) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
(H9)
by (f_equal . . . . . H8)
we proved eq T t2 (lift (S n) O x2)
eq T (λe:T.e t2) (λe:T.e (lift (S n) O x2))
end of H9
(H10)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove getl n c0 (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c0 (CHead x0 (Bind Abbr) x1)
end of H10
(H11)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead x0 (Bind Abbr) x1)
end of H11
(h1)
(H12)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u0 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead x0 (Bind Abbr) x1)
end of H12
suppose H13: eq C d x0
(H14)
consider H12
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 x1
by (eq_ind_r . . . H10 . previous)
getl n c0 (CHead x0 (Bind Abbr) u0)
end of H14
(H15)
consider H12
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 x1
by (eq_ind_r . . . H7 . previous)
sty0 g x0 u0 x2
end of H15
(H16)
by (eq_ind_r . . . H14 . H13)
getl n c0 (CHead d (Bind Abbr) u0)
end of H16
(H17)
by (eq_ind_r . . . H15 . H13)
sty0 g d u0 x2
end of H17
by (H2 . H17)
we proved ty3 g d u0 x2
by (ty3_abbr . . . . . H16 . previous)
we proved ty3 g c0 (TLRef n) (lift (S n) O x2)
(eq C d x0)→(ty3 g c0 (TLRef n) (lift (S n) O x2))
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq C d x0
end of h2
by (h1 h2)
we proved ty3 g c0 (TLRef n) (lift (S n) O x2)
by (eq_ind_r . . . previous . H9)
ty3 g c0 (TLRef n) t2
ty3 g c0 (TLRef n) t2
case or_intror : H5:ex3_3 C T T λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abst) u1) λe:C.λu1:T.λt0:T.sty0 g e u1 t0 λ:C.λu1:T.λ:T.eq T t2 (lift (S n) O u1) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
we proceed by induction on H5 to prove ty3 g c0 (TLRef n) t2
case ex3_3_intro : x0:C x1:T x2:T H6:getl n c0 (CHead x0 (Bind Abst) x1) :sty0 g x0 x1 x2 H8:eq T t2 (lift (S n) O x1) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
(H9)
by (f_equal . . . . . H8)
we proved eq T t2 (lift (S n) O x1)
eq T (λe:T.e t2) (λe:T.e (lift (S n) O x1))
end of H9
(H11)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abst) x1)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H11
consider H11
we proved
<λ:C.Prop>
CASE CHead x0 (Bind Abst) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift (S n) O x1)
we proved ty3 g c0 (TLRef n) (lift (S n) O x1)
by (eq_ind_r . . . previous . H9)
ty3 g c0 (TLRef n) t2
ty3 g c0 (TLRef n) t2
we proved ty3 g c0 (TLRef n) t2
∀t2:T.∀H3:(sty0 g c0 (TLRef n) t2).(ty3 g c0 (TLRef n) t2)
case ty3_abst : n:nat c0:C d:C u0:T H0:getl n c0 (CHead d (Bind Abst) u0) t:T H1:ty3 g d u0 t ⇒
the thesis becomes ∀t2:T.∀H3:(sty0 g c0 (TLRef n) t2).(ty3 g c0 (TLRef n) t2)
() by induction hypothesis we know ∀t2:T.(sty0 g d u0 t2)→(ty3 g d u0 t2)
assume t2: T
suppose H3: sty0 g c0 (TLRef n) t2
(H_x)
by (sty0_gen_lref . . . . H3)
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T t2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T t2 (lift (S n) O u)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove ty3 g c0 (TLRef n) t2
case or_introl : H5:ex3_3 C T T λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abbr) u1) λe:C.λu1:T.λt0:T.sty0 g e u1 t0 λ:C.λ:T.λt0:T.eq T t2 (lift (S n) O t0) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
we proceed by induction on H5 to prove ty3 g c0 (TLRef n) t2
case ex3_3_intro : x0:C x1:T x2:T H6:getl n c0 (CHead x0 (Bind Abbr) x1) :sty0 g x0 x1 x2 H8:eq T t2 (lift (S n) O x2) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
(H9)
by (f_equal . . . . . H8)
we proved eq T t2 (lift (S n) O x2)
eq T (λe:T.e t2) (λe:T.e (lift (S n) O x2))
end of H9
(H11)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u0) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H11
consider H11
we proved
<λ:C.Prop>
CASE CHead x0 (Bind Abbr) x1 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift (S n) O x2)
we proved ty3 g c0 (TLRef n) (lift (S n) O x2)
by (eq_ind_r . . . previous . H9)
ty3 g c0 (TLRef n) t2
ty3 g c0 (TLRef n) t2
case or_intror : H5:ex3_3 C T T λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abst) u1) λe:C.λu1:T.λt0:T.sty0 g e u1 t0 λ:C.λu1:T.λ:T.eq T t2 (lift (S n) O u1) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
we proceed by induction on H5 to prove ty3 g c0 (TLRef n) t2
case ex3_3_intro : x0:C x1:T x2:T H6:getl n c0 (CHead x0 (Bind Abst) x1) H7:sty0 g x0 x1 x2 H8:eq T t2 (lift (S n) O x1) ⇒
the thesis becomes ty3 g c0 (TLRef n) t2
(H9)
by (f_equal . . . . . H8)
we proved eq T t2 (lift (S n) O x1)
eq T (λe:T.e t2) (λe:T.e (lift (S n) O x1))
end of H9
(H10)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
we proceed by induction on the previous result to prove getl n c0 (CHead x0 (Bind Abst) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c0 (CHead x0 (Bind Abst) x1)
end of H10
(H11)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abst) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead x0 (Bind Abst) x1)
end of H11
(h1)
(H12)
by (getl_mono . . . H0 . H6)
we proved eq C (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u0 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead d (Bind Abst) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead x0 (Bind Abst) x1)
end of H12
suppose H13: eq C d x0
(H14)
consider H12
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 x1
by (eq_ind_r . . . H10 . previous)
getl n c0 (CHead x0 (Bind Abst) u0)
end of H14
(H15)
consider H12
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 x1
by (eq_ind_r . . . H7 . previous)
sty0 g x0 u0 x2
end of H15
consider H12
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abst) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 x1
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift (S n) O x1)
case refl_equal : ⇒
the thesis becomes ty3 g c0 (TLRef n) (lift (S n) O u0)
(H16)
by (eq_ind_r . . . H14 . H13)
getl n c0 (CHead d (Bind Abst) u0)
end of H16
by (ty3_abst . . . . . H16 . H1)
ty3 g c0 (TLRef n) (lift (S n) O u0)
we proved ty3 g c0 (TLRef n) (lift (S n) O x1)
(eq C d x0)→(ty3 g c0 (TLRef n) (lift (S n) O x1))
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abst) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead x0 (Bind Abst) x1 OF CSort ⇒d | CHead c1 ⇒c1
eq C d x0
end of h2
by (h1 h2)
we proved ty3 g c0 (TLRef n) (lift (S n) O x1)
by (eq_ind_r . . . previous . H9)
ty3 g c0 (TLRef n) t2
ty3 g c0 (TLRef n) t2
we proved ty3 g c0 (TLRef n) t2
∀t2:T.∀H3:(sty0 g c0 (TLRef n) t2).(ty3 g c0 (TLRef n) t2)
case ty3_bind : c0:C u0:T t:T H0:ty3 g c0 u0 t b:B t2:T t3:T :ty3 g (CHead c0 (Bind b) u0) t2 t3 ⇒
the thesis becomes ∀t0:T.∀H4:(sty0 g c0 (THead (Bind b) u0 t2) t0).(ty3 g c0 (THead (Bind b) u0 t2) t0)
() by induction hypothesis we know ∀t2:T.(sty0 g c0 u0 t2)→(ty3 g c0 u0 t2)
(H3) by induction hypothesis we know ∀t4:T.(sty0 g (CHead c0 (Bind b) u0) t2 t4)→(ty3 g (CHead c0 (Bind b) u0) t2 t4)
assume t0: T
suppose H4: sty0 g c0 (THead (Bind b) u0 t2) t0
(H_x)
by (sty0_gen_bind . . . . . . H4)
ex2 T λt2:T.sty0 g (CHead c0 (Bind b) u0) t2 t2 λt2:T.eq T t0 (THead (Bind b) u0 t2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove ty3 g c0 (THead (Bind b) u0 t2) t0
case ex_intro2 : x:T H6:sty0 g (CHead c0 (Bind b) u0) t2 x H7:eq T t0 (THead (Bind b) u0 x) ⇒
the thesis becomes ty3 g c0 (THead (Bind b) u0 t2) t0
(H8)
by (f_equal . . . . . H7)
we proved eq T t0 (THead (Bind b) u0 x)
eq T (λe:T.e t0) (λe:T.e (THead (Bind b) u0 x))
end of H8
by (H3 . H6)
we proved ty3 g (CHead c0 (Bind b) u0) t2 x
by (ty3_bind . . . . H0 . . . previous)
we proved ty3 g c0 (THead (Bind b) u0 t2) (THead (Bind b) u0 x)
by (eq_ind_r . . . previous . H8)
ty3 g c0 (THead (Bind b) u0 t2) t0
we proved ty3 g c0 (THead (Bind b) u0 t2) t0
∀t0:T.∀H4:(sty0 g c0 (THead (Bind b) u0 t2) t0).(ty3 g c0 (THead (Bind b) u0 t2) t0)
case ty3_appl : c0:C w:T u0:T H0:ty3 g c0 w u0 v:T t:T H2:ty3 g c0 v (THead (Bind Abst) u0 t) ⇒
the thesis becomes ∀t2:T.∀H4:(sty0 g c0 (THead (Flat Appl) w v) t2).(ty3 g c0 (THead (Flat Appl) w v) t2)
() by induction hypothesis we know ∀t2:T.(sty0 g c0 w t2)→(ty3 g c0 w t2)
(H3) by induction hypothesis we know ∀t2:T.(sty0 g c0 v t2)→(ty3 g c0 v t2)
assume t2: T
suppose H4: sty0 g c0 (THead (Flat Appl) w v) t2
(H_x)
by (sty0_gen_appl . . . . . H4)
ex2 T λt2:T.sty0 g c0 v t2 λt2:T.eq T t2 (THead (Flat Appl) w t2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove ty3 g c0 (THead (Flat Appl) w v) t2
case ex_intro2 : x:T H6:sty0 g c0 v x H7:eq T t2 (THead (Flat Appl) w x) ⇒
the thesis becomes ty3 g c0 (THead (Flat Appl) w v) t2
(H8)
by (f_equal . . . . . H7)
we proved eq T t2 (THead (Flat Appl) w x)
eq T (λe:T.e t2) (λe:T.e (THead (Flat Appl) w x))
end of H8
(H_y) by (H3 . H6) we proved ty3 g c0 v x
(H9)
by (ty3_unique . . . . H_y . H2)
pc3 c0 x (THead (Bind Abst) u0 t)
end of H9
by (ty3_correct . . . . H_y)
we proved ex T λt:T.ty3 g c0 x t
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
case ex_intro : x0:T H10:ty3 g c0 x x0 ⇒
the thesis becomes ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
by (ty3_correct . . . . H0)
we proved ex T λt:T.ty3 g c0 u0 t
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
case ex_intro : x1:T :ty3 g c0 u0 x1 ⇒
the thesis becomes ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
by (ty3_correct . . . . H2)
we proved ex T λt:T.ty3 g c0 (THead (Bind Abst) u0 t) t
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
case ex_intro : x2:T H12:ty3 g c0 (THead (Bind Abst) u0 t) x2 ⇒
the thesis becomes ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
by (ty3_gen_bind . . . . . . H12)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c0 (THead (Bind Abst) u0 t2) x2
λ:T.λt:T.ty3 g c0 u0 t
λt2:T.λ:T.ty3 g (CHead c0 (Bind Abst) u0) t t2
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
case ex3_2_intro : x3:T x4:T :pc3 c0 (THead (Bind Abst) u0 x3) x2 H14:ty3 g c0 u0 x4 H15:ty3 g (CHead c0 (Bind Abst) u0) t x3 ⇒
the thesis becomes ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
(h1)
by (ty3_bind . . . . H14 . . . H15)
we proved ty3 g c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) u0 x3)
by (ty3_sconv . . . . H10 . . previous H9)
we proved ty3 g c0 x (THead (Bind Abst) u0 x3)
by (ty3_appl . . . . H0 . . previous)
ty3
g
c0
THead (Flat Appl) w x
THead (Flat Appl) w (THead (Bind Abst) u0 x3)
end of h1
(h2)
by (ty3_appl . . . . H0 . . H2)
ty3
g
c0
THead (Flat Appl) w v
THead (Flat Appl) w (THead (Bind Abst) u0 t)
end of h2
(h3)
by (ty3_unique . . . . H2 . H_y)
we proved pc3 c0 (THead (Bind Abst) u0 t) x
by (pc3_thin_dx . . . previous . .)
pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t)
THead (Flat Appl) w x
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
we proved ty3 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w x)
by (eq_ind_r . . . previous . H8)
ty3 g c0 (THead (Flat Appl) w v) t2
we proved ty3 g c0 (THead (Flat Appl) w v) t2
∀t2:T.∀H4:(sty0 g c0 (THead (Flat Appl) w v) t2).(ty3 g c0 (THead (Flat Appl) w v) t2)
case ty3_cast : c0:C t2:T t3:T H0:ty3 g c0 t2 t3 t0:T :ty3 g c0 t3 t0 ⇒
the thesis becomes ∀t4:T.∀H4:(sty0 g c0 (THead (Flat Cast) t3 t2) t4).(ty3 g c0 (THead (Flat Cast) t3 t2) t4)
(H1) by induction hypothesis we know ∀t4:T.(sty0 g c0 t2 t4)→(ty3 g c0 t2 t4)
(H3) by induction hypothesis we know ∀t4:T.(sty0 g c0 t3 t4)→(ty3 g c0 t3 t4)
assume t4: T
suppose H4: sty0 g c0 (THead (Flat Cast) t3 t2) t4
(H_x)
by (sty0_gen_cast . . . . . H4)
ex3_2 T T λv2:T.λ:T.sty0 g c0 t3 v2 λ:T.λt2:T.sty0 g c0 t2 t2 λv2:T.λt2:T.eq T t4 (THead (Flat Cast) v2 t2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove ty3 g c0 (THead (Flat Cast) t3 t2) t4
case ex3_2_intro : x0:T x1:T H6:sty0 g c0 t3 x0 H7:sty0 g c0 t2 x1 H8:eq T t4 (THead (Flat Cast) x0 x1) ⇒
the thesis becomes ty3 g c0 (THead (Flat Cast) t3 t2) t4
(H9)
by (f_equal . . . . . H8)
we proved eq T t4 (THead (Flat Cast) x0 x1)
eq T (λe:T.e t4) (λe:T.e (THead (Flat Cast) x0 x1))
end of H9
(H_y) by (H1 . H7) we proved ty3 g c0 t2 x1
(H_y0) by (H3 . H6) we proved ty3 g c0 t3 x0
(H10)
by (ty3_unique . . . . H_y . H0)
pc3 c0 x1 t3
end of H10
by (ty3_correct . . . . H_y0)
we proved ex T λt:T.ty3 g c0 x0 t
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
case ex_intro : x:T H11:ty3 g c0 x0 x ⇒
the thesis becomes ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
by (ty3_correct . . . . H_y)
we proved ex T λt:T.ty3 g c0 x1 t
we proceed by induction on the previous result to prove ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
case ex_intro : x2:T H12:ty3 g c0 x1 x2 ⇒
the thesis becomes ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
(h1)
by (ty3_sconv . . . . H12 . . H_y0 H10)
we proved ty3 g c0 x1 x0
by (ty3_cast . . . . previous . H11)
ty3 g c0 (THead (Flat Cast) x0 x1) (THead (Flat Cast) x x0)
end of h1
(h2)
by (ty3_cast . . . . H0 . H_y0)
ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 t3)
end of h2
(h3)
by (ty3_unique . . . . H0 . H_y)
we proved pc3 c0 t3 x1
by (pc3_thin_dx . . . previous . .)
pc3 c0 (THead (Flat Cast) x0 t3) (THead (Flat Cast) x0 x1)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
we proved ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 x1)
by (eq_ind_r . . . previous . H9)
ty3 g c0 (THead (Flat Cast) t3 t2) t4
we proved ty3 g c0 (THead (Flat Cast) t3 t2) t4
∀t4:T.∀H4:(sty0 g c0 (THead (Flat Cast) t3 t2) t4).(ty3 g c0 (THead (Flat Cast) t3 t2) t4)
we proved ∀t2:T.(sty0 g c u t2)→(ty3 g c u t2)
we proved ∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(sty0 g c u t2)→(ty3 g c u t2)