DEFINITION ty3_unique()
TYPE =
∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(ty3 g c u t2)→(pc3 c t1 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.(ty3 g c u t2)→(pc3 c t1 t2)
case ty3_conv : c0:C t2:T t:T :ty3 g c0 t2 t u0:T t0:T :ty3 g c0 u0 t0 H4:pc3 c0 t0 t2 ⇒
the thesis becomes ∀t3:T.∀H5:(ty3 g c0 u0 t3).(pc3 c0 t2 t3)
() by induction hypothesis we know ∀t3:T.(ty3 g c0 t2 t3)→(pc3 c0 t t3)
(H3) by induction hypothesis we know ∀t3:T.(ty3 g c0 u0 t3)→(pc3 c0 t0 t3)
assume t3: T
suppose H5: ty3 g c0 u0 t3
(h1) by (pc3_s . . . H4) we proved pc3 c0 t2 t0
(h2) by (H3 . H5) we proved pc3 c0 t0 t3
by (pc3_t . . . h1 . h2)
we proved pc3 c0 t2 t3
∀t3:T.∀H5:(ty3 g c0 u0 t3).(pc3 c0 t2 t3)
case ty3_sort : c0:C m:nat ⇒
the thesis becomes ∀t2:T.∀H0:(ty3 g c0 (TSort m) t2).(pc3 c0 (TSort (next g m)) t2)
assume t2: T
suppose H0: ty3 g c0 (TSort m) t2
by (ty3_gen_sort . . . . H0)
we proved pc3 c0 (TSort (next g m)) t2
∀t2:T.∀H0:(ty3 g c0 (TSort m) t2).(pc3 c0 (TSort (next g 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:(ty3 g c0 (TLRef n) t2).(pc3 c0 (lift (S n) O t) t2)
(H2) by induction hypothesis we know ∀t2:T.(ty3 g d u0 t2)→(pc3 d t t2)
assume t2: T
suppose H3: ty3 g c0 (TLRef n) t2
by (ty3_gen_lref . . . . H3)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proceed by induction on the previous result to prove pc3 c0 (lift (S n) O t) t2
case or_introl : H4:ex3_3 C T T λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2 λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abbr) u1) λe:C.λu1:T.λt0:T.ty3 g e u1 t0 ⇒
the thesis becomes pc3 c0 (lift (S n) O t) t2
we proceed by induction on H4 to prove pc3 c0 (lift (S n) O t) t2
case ex3_3_intro : x0:C x1:T x2:T H5:pc3 c0 (lift (S n) O x2) t2 H6:getl n c0 (CHead x0 (Bind Abbr) x1) H7:ty3 g x0 x1 x2 ⇒
the thesis becomes pc3 c0 (lift (S n) O t) t2
(H8)
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 H8
(H9)
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 H9
(h1)
(H10)
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 H10
suppose H11: eq C d x0
(H12)
consider H10
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 . . . H8 . previous)
getl n c0 (CHead x0 (Bind Abbr) u0)
end of H12
(H13)
consider H10
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)
ty3 g x0 u0 x2
end of H13
(H14)
by (eq_ind_r . . . H12 . H11)
getl n c0 (CHead d (Bind Abbr) u0)
end of H14
(H15)
by (eq_ind_r . . . H13 . H11)
ty3 g d u0 x2
end of H15
(h1)
by (getl_drop . . . . . H14)
drop (S n) O c0 d
end of h1
(h2) by (H2 . H15) we proved pc3 d t x2
by (pc3_lift . . . . h1 . . h2)
we proved pc3 c0 (lift (S n) O t) (lift (S n) O x2)
by (pc3_t . . . previous . H5)
we proved pc3 c0 (lift (S n) O t) t2
(eq C d x0)→(pc3 c0 (lift (S n) O t) t2)
end of h1
(h2)
consider H9
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)
pc3 c0 (lift (S n) O t) t2
pc3 c0 (lift (S n) O t) t2
case or_intror : H4:ex3_3 C T T λ:C.λu1:T.λ:T.pc3 c0 (lift (S n) O u1) t2 λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abst) u1) λe:C.λu1:T.λt0:T.ty3 g e u1 t0 ⇒
the thesis becomes pc3 c0 (lift (S n) O t) t2
we proceed by induction on H4 to prove pc3 c0 (lift (S n) O t) t2
case ex3_3_intro : x0:C x1:T x2:T :pc3 c0 (lift (S n) O x1) t2 H6:getl n c0 (CHead x0 (Bind Abst) x1) :ty3 g x0 x1 x2 ⇒
the thesis becomes pc3 c0 (lift (S n) O t) t2
(H9)
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 H9
consider H9
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 pc3 c0 (lift (S n) O t) t2
pc3 c0 (lift (S n) O t) t2
pc3 c0 (lift (S n) O t) t2
we proved pc3 c0 (lift (S n) O t) t2
∀t2:T.∀H3:(ty3 g c0 (TLRef n) t2).(pc3 c0 (lift (S n) O t) t2)
case ty3_abst : n:nat c0:C d:C u0:T H0:getl n c0 (CHead d (Bind Abst) u0) t:T :ty3 g d u0 t ⇒
the thesis becomes ∀t2:T.∀H3:(ty3 g c0 (TLRef n) t2).(pc3 c0 (lift (S n) O u0) t2)
() by induction hypothesis we know ∀t2:T.(ty3 g d u0 t2)→(pc3 d t t2)
assume t2: T
suppose H3: ty3 g c0 (TLRef n) t2
by (ty3_gen_lref . . . . H3)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proceed by induction on the previous result to prove pc3 c0 (lift (S n) O u0) t2
case or_introl : H4:ex3_3 C T T λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2 λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abbr) u1) λe:C.λu1:T.λt0:T.ty3 g e u1 t0 ⇒
the thesis becomes pc3 c0 (lift (S n) O u0) t2
we proceed by induction on H4 to prove pc3 c0 (lift (S n) O u0) t2
case ex3_3_intro : x0:C x1:T x2:T :pc3 c0 (lift (S n) O x2) t2 H6:getl n c0 (CHead x0 (Bind Abbr) x1) :ty3 g x0 x1 x2 ⇒
the thesis becomes pc3 c0 (lift (S n) O u0) t2
(H9)
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 H9
consider H9
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 pc3 c0 (lift (S n) O u0) t2
pc3 c0 (lift (S n) O u0) t2
pc3 c0 (lift (S n) O u0) t2
case or_intror : H4:ex3_3 C T T λ:C.λu1:T.λ:T.pc3 c0 (lift (S n) O u1) t2 λe:C.λu1:T.λ:T.getl n c0 (CHead e (Bind Abst) u1) λe:C.λu1:T.λt0:T.ty3 g e u1 t0 ⇒
the thesis becomes pc3 c0 (lift (S n) O u0) t2
we proceed by induction on H4 to prove pc3 c0 (lift (S n) O u0) t2
case ex3_3_intro : x0:C x1:T x2:T H5:pc3 c0 (lift (S n) O x1) t2 H6:getl n c0 (CHead x0 (Bind Abst) x1) H7:ty3 g x0 x1 x2 ⇒
the thesis becomes pc3 c0 (lift (S n) O u0) t2
(H8)
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 H8
(H9)
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 H9
(h1)
(H10)
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 H10
suppose H11: eq C d x0
(H12)
consider H10
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 . . . H8 . previous)
getl n c0 (CHead x0 (Bind Abst) u0)
end of H12
(H13)
consider H10
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)
ty3 g x0 u0 x2
end of H13
(H14)
consider H10
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 . . . H5 . previous)
pc3 c0 (lift (S n) O u0) t2
end of H14
consider H14
we proved pc3 c0 (lift (S n) O u0) t2
(eq C d x0)→(pc3 c0 (lift (S n) O u0) t2)
end of h1
(h2)
consider H9
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)
pc3 c0 (lift (S n) O u0) t2
pc3 c0 (lift (S n) O u0) t2
we proved pc3 c0 (lift (S n) O u0) t2
∀t2:T.∀H3:(ty3 g c0 (TLRef n) t2).(pc3 c0 (lift (S n) O u0) t2)
case ty3_bind : c0:C u0:T t:T :ty3 g c0 u0 t b:B t0:T t2:T :ty3 g (CHead c0 (Bind b) u0) t0 t2 ⇒
the thesis becomes ∀t3:T.∀H4:(ty3 g c0 (THead (Bind b) u0 t0) t3).(pc3 c0 (THead (Bind b) u0 t2) t3)
() by induction hypothesis we know ∀t2:T.(ty3 g c0 u0 t2)→(pc3 c0 t t2)
(H3) by induction hypothesis we know ∀t3:T.(ty3 g (CHead c0 (Bind b) u0) t0 t3)→(pc3 (CHead c0 (Bind b) u0) t2 t3)
assume t3: T
suppose H4: ty3 g c0 (THead (Bind b) u0 t0) t3
by (ty3_gen_bind . . . . . . H4)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c0 (THead (Bind b) u0 t2) t3
λ:T.λt:T.ty3 g c0 u0 t
λt2:T.λ:T.ty3 g (CHead c0 (Bind b) u0) t0 t2
we proceed by induction on the previous result to prove pc3 c0 (THead (Bind b) u0 t2) t3
case ex3_2_intro : x0:T x1:T H5:pc3 c0 (THead (Bind b) u0 x0) t3 :ty3 g c0 u0 x1 H7:ty3 g (CHead c0 (Bind b) u0) t0 x0 ⇒
the thesis becomes pc3 c0 (THead (Bind b) u0 t2) t3
by (H3 . H7)
we proved pc3 (CHead c0 (Bind b) u0) t2 x0
by (pc3_head_2 . . . . . previous)
we proved pc3 c0 (THead (Bind b) u0 t2) (THead (Bind b) u0 x0)
by (pc3_t . . . previous . H5)
pc3 c0 (THead (Bind b) u0 t2) t3
we proved pc3 c0 (THead (Bind b) u0 t2) t3
∀t3:T.∀H4:(ty3 g c0 (THead (Bind b) u0 t0) t3).(pc3 c0 (THead (Bind b) u0 t2) t3)
case ty3_appl : c0:C w:T u0:T :ty3 g c0 w u0 v:T t:T :ty3 g c0 v (THead (Bind Abst) u0 t) ⇒
the thesis becomes
∀t2:T
.∀H4:ty3 g c0 (THead (Flat Appl) w v) t2
.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
() by induction hypothesis we know ∀t2:T.(ty3 g c0 w t2)→(pc3 c0 u0 t2)
(H3) by induction hypothesis we know ∀t2:T.(ty3 g c0 v t2)→(pc3 c0 (THead (Bind Abst) u0 t) t2)
assume t2: T
suppose H4: ty3 g c0 (THead (Flat Appl) w v) t2
by (ty3_gen_appl . . . . . H4)
we proved
ex3_2
T
T
λu:T.λt:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t2
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
we proceed by induction on the previous result to prove pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
case ex3_2_intro : x0:T x1:T H5:pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t2 H6:ty3 g c0 v (THead (Bind Abst) x0 x1) :ty3 g c0 w x0 ⇒
the thesis becomes pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
by (H3 . H6)
we proved pc3 c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0 x1)
by (pc3_thin_dx . . . previous . .)
we proved
pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t)
THead (Flat Appl) w (THead (Bind Abst) x0 x1)
by (pc3_t . . . previous . H5)
pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
we proved pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
∀t2:T
.∀H4:ty3 g c0 (THead (Flat Appl) w v) t2
.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) t2
case ty3_cast : c0:C t0:T t2:T :ty3 g c0 t0 t2 t3:T :ty3 g c0 t2 t3 ⇒
the thesis becomes ∀t4:T.∀H4:(ty3 g c0 (THead (Flat Cast) t2 t0) t4).(pc3 c0 (THead (Flat Cast) t3 t2) t4)
() by induction hypothesis we know ∀t3:T.(ty3 g c0 t0 t3)→(pc3 c0 t2 t3)
(H3) by induction hypothesis we know ∀t4:T.(ty3 g c0 t2 t4)→(pc3 c0 t3 t4)
assume t4: T
suppose H4: ty3 g c0 (THead (Flat Cast) t2 t0) t4
by (ty3_gen_cast . . . . . H4)
we proved ex3 T λt0:T.pc3 c0 (THead (Flat Cast) t0 t2) t4 λ:T.ty3 g c0 t0 t2 λt0:T.ty3 g c0 t2 t0
we proceed by induction on the previous result to prove pc3 c0 (THead (Flat Cast) t3 t2) t4
case ex3_intro : x0:T H5:pc3 c0 (THead (Flat Cast) x0 t2) t4 :ty3 g c0 t0 t2 H7:ty3 g c0 t2 x0 ⇒
the thesis becomes pc3 c0 (THead (Flat Cast) t3 t2) t4
by (H3 . H7)
we proved pc3 c0 t3 x0
by (pc3_head_1 . . . previous . .)
we proved pc3 c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) x0 t2)
by (pc3_t . . . previous . H5)
pc3 c0 (THead (Flat Cast) t3 t2) t4
we proved pc3 c0 (THead (Flat Cast) t3 t2) t4
∀t4:T.∀H4:(ty3 g c0 (THead (Flat Cast) t2 t0) t4).(pc3 c0 (THead (Flat Cast) t3 t2) t4)
we proved ∀t2:T.(ty3 g c u t2)→(pc3 c t1 t2)
we proved ∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(ty3 g c u t2)→(pc3 c t1 t2)