DEFINITION ty3_gen_appl()
TYPE =
∀g:G
.∀c:C
.∀w:T
.∀v:T
.∀x:T
.ty3 g c (THead (Flat Appl) w v) x
→(ex3_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u)
BODY =
assume g: G
assume c: C
assume w: T
assume v: T
assume x: T
suppose H: ty3 g c (THead (Flat Appl) w v) x
assume y: T
suppose H0: ty3 g c y x
we proceed by induction on H0 to prove
eq T y (THead (Flat Appl) w v)
→(ex3_2
T
T
λu:T.λt1:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t1)) x
λu:T.λt1:T.ty3 g c v (THead (Bind Abst) u t1)
λu:T.λ:T.ty3 g c w u)
case ty3_conv : c0:C t2:T t:T :ty3 g c0 t2 t u:T t1:T H3:ty3 g c0 u t1 H5:pc3 c0 t1 t2 ⇒
the thesis becomes
∀H6:eq T u (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
() by induction hypothesis we know
eq T t2 (THead (Flat Appl) w v)
→(ex3_2
T
T
λu:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t0)) t
λu:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u t0)
λu:T.λ:T.ty3 g c0 w u)
(H4) by induction hypothesis we know
eq T u (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t1
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0)
suppose H6: eq T u (THead (Flat Appl) w v)
(H7)
by (f_equal . . . . . H6)
we proved eq T u (THead (Flat Appl) w v)
eq T (λe:T.e u) (λe:T.e (THead (Flat Appl) w v))
end of H7
(H8)
we proceed by induction on H7 to prove
eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt3:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t3)) t1
λu0:T.λt3:T.ty3 g c0 v (THead (Bind Abst) u0 t3)
λu0:T.λ:T.ty3 g c0 w u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt3:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t3)) t1
λu0:T.λt3:T.ty3 g c0 v (THead (Bind Abst) u0 t3)
λu0:T.λ:T.ty3 g c0 w u0)
end of H8
(H10)
by (refl_equal . .)
we proved eq T (THead (Flat Appl) w v) (THead (Flat Appl) w v)
by (H8 previous)
ex3_2
T
T
λu0:T.λt3:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t3)) t1
λu0:T.λt3:T.ty3 g c0 v (THead (Bind Abst) u0 t3)
λu0:T.λ:T.ty3 g c0 w u0
end of H10
we proceed by induction on H10 to prove
ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
case ex3_2_intro : x0:T x1:T H11:pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t1 H12:ty3 g c0 v (THead (Bind Abst) x0 x1) H13:ty3 g c0 w x0 ⇒
the thesis becomes
ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
by (pc3_t . . . H11 . H5)
we proved pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t2
by (ex3_2_intro . . . . . . . previous H12 H13)
ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
we proved
ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
∀H6:eq T u (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀H1:eq T (TSort m) (THead (Flat Appl) w v)
.ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
TSort (next g m)
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
suppose H1: eq T (TSort m) (THead (Flat Appl) w v)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort m OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort m OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
TSort (next g m)
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
we proved
ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
TSort (next g m)
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
∀H1:eq T (TSort m) (THead (Flat Appl) w v)
.ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
TSort (next g m)
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
case ty3_abbr : n:nat c0:C d:C u:T :getl n c0 (CHead d (Bind Abbr) u) t:T :ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
() by induction hypothesis we know
eq T u (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt0:T.pc3 d (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t
λu0:T.λt0:T.ty3 g d v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g d w u0)
suppose H4: eq T (TLRef n) (THead (Flat Appl) w v)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
we proved
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
∀H4:eq T (TLRef n) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
case ty3_abst : n:nat c0:C d:C u:T :getl n c0 (CHead d (Bind Abst) u) t:T :ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O u
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
() by induction hypothesis we know
eq T u (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt0:T.pc3 d (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t
λu0:T.λt0:T.ty3 g d v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g d w u0)
suppose H4: eq T (TLRef n) (THead (Flat Appl) w v)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O u
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
we proved
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O u
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
∀H4:eq T (TLRef n) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
lift (S n) O u
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
case ty3_bind : c0:C u:T t:T :ty3 g c0 u t b:B t1:T t2:T :ty3 g (CHead c0 (Bind b) u) t1 t2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind b) u t1) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Bind b) u t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
() by induction hypothesis we know
eq T u (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt0:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0)
() by induction hypothesis we know
eq T t1 (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T
.λt0:T
.pc3
CHead c0 (Bind b) u
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
t2
λu0:T.λt0:T.ty3 g (CHead c0 (Bind b) u) v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g (CHead c0 (Bind b) u) w u0)
suppose H5: eq T (THead (Bind b) u t1) (THead (Flat Appl) w v)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Bind b) u t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
we proved
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Bind b) u t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
∀H5:eq T (THead (Bind b) u t1) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Bind b) u t2
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
case ty3_appl : c0:C w0:T u:T H1:ty3 g c0 w0 u v0:T t:T H3:ty3 g c0 v0 (THead (Bind Abst) u t) ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) w0 v0) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt1:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t1)
THead (Flat Appl) w0 (THead (Bind Abst) u t)
λu0:T.λt1:T.ty3 g c0 v (THead (Bind Abst) u0 t1)
λu0:T.λ:T.ty3 g c0 w u0
(H2) by induction hypothesis we know
eq T w0 (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T.λt:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) u
λu0:T.λt:T.ty3 g c0 v (THead (Bind Abst) u0 t)
λu0:T.λ:T.ty3 g c0 w u0)
(H4) by induction hypothesis we know
eq T v0 (THead (Flat Appl) w v)
→(ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Bind Abst) u t
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0)
suppose H5: eq T (THead (Flat Appl) w0 v0) (THead (Flat Appl) w v)
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) w0 v0 OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
THead (Flat Appl) w0 v0
λe:T.<λ:T.T> CASE e OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
THead (Flat Appl) w v
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) w0 v0 OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
THead (Flat Appl) w0 v0
λe:T.<λ:T.T> CASE e OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
THead (Flat Appl) w v
end of H7
suppose H8: eq T w0 w
(H10)
consider H7
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) w0 v0 OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒v0 | TLRef ⇒v0 | THead t0⇒t0
that is equivalent to eq T v0 v
we proceed by induction on the previous result to prove ty3 g c0 v (THead (Bind Abst) u t)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
ty3 g c0 v (THead (Bind Abst) u t)
end of H10
(H12)
we proceed by induction on H8 to prove ty3 g c0 w u
case refl_equal : ⇒
the thesis becomes the hypothesis H1
ty3 g c0 w u
end of H12
by (pc3_refl . .)
we proved
pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead (Flat Appl) w (THead (Bind Abst) u t)
by (ex3_2_intro . . . . . . . previous H10 H12)
we proved
ex3_2
T
T
λu0:T
.λt0:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t0)
THead (Flat Appl) w (THead (Bind Abst) u t)
λu0:T.λt0:T.ty3 g c0 v (THead (Bind Abst) u0 t0)
λu0:T.λ:T.ty3 g c0 w u0
by (eq_ind_r . . . previous . H8)
we proved
ex3_2
T
T
λu0:T
.λt1:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t1)
THead (Flat Appl) w0 (THead (Bind Abst) u t)
λu0:T.λt1:T.ty3 g c0 v (THead (Bind Abst) u0 t1)
λu0:T.λ:T.ty3 g c0 w u0
eq T w0 w
→(ex3_2
T
T
λu0:T
.λt1:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t1)
THead (Flat Appl) w0 (THead (Bind Abst) u t)
λu0:T.λt1:T.ty3 g c0 v (THead (Bind Abst) u0 t1)
λu0:T.λ:T.ty3 g c0 w u0)
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) w0 v0 OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Flat Appl) w v OF TSort ⇒w0 | TLRef ⇒w0 | THead t0 ⇒t0
eq T w0 w
end of h2
by (h1 h2)
we proved
ex3_2
T
T
λu0:T
.λt1:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t1)
THead (Flat Appl) w0 (THead (Bind Abst) u t)
λu0:T.λt1:T.ty3 g c0 v (THead (Bind Abst) u0 t1)
λu0:T.λ:T.ty3 g c0 w u0
∀H5:eq T (THead (Flat Appl) w0 v0) (THead (Flat Appl) w v)
.ex3_2
T
T
λu0:T
.λt1:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u0 t1)
THead (Flat Appl) w0 (THead (Bind Abst) u t)
λu0:T.λt1:T.ty3 g c0 v (THead (Bind Abst) u0 t1)
λu0:T.λ:T.ty3 g c0 w u0
case ty3_cast : c0:C t1:T t2:T :ty3 g c0 t1 t2 t0:T :ty3 g c0 t2 t0 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) t2 t1) (THead (Flat Appl) w v)
.ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead (Flat Cast) t0 t2
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
() by induction hypothesis we know
eq T t1 (THead (Flat Appl) w v)
→(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)
() by induction hypothesis we know
eq T t2 (THead (Flat Appl) w v)
→(ex3_2
T
T
λu:T.λt:T.pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u)
suppose H5: eq T (THead (Flat Cast) t2 t1) (THead (Flat Appl) w v)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) t2 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) t2 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Flat Appl) w v OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒False | Cast⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead (Flat Cast) t0 t2
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
we proved
ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead (Flat Cast) t0 t2
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
∀H5:eq T (THead (Flat Cast) t2 t1) (THead (Flat Appl) w v)
.ex3_2
T
T
λu:T
.λt:T
.pc3
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead (Flat Cast) t0 t2
λu:T.λt:T.ty3 g c0 v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c0 w u
we proved
eq T y (THead (Flat Appl) w v)
→(ex3_2
T
T
λu:T.λt1:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t1)) x
λu:T.λt1:T.ty3 g c v (THead (Bind Abst) u t1)
λu:T.λ:T.ty3 g c w u)
we proved
∀y:T
.ty3 g c y x
→(eq T y (THead (Flat Appl) w v)
→(ex3_2
T
T
λu:T.λt1:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t1)) x
λu:T.λt1:T.ty3 g c v (THead (Bind Abst) u t1)
λu:T.λ:T.ty3 g c w u))
by (insert_eq . . . . previous H)
we proved
ex3_2
T
T
λu:T.λt0:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) x
λu:T.λt0:T.ty3 g c v (THead (Bind Abst) u t0)
λu:T.λ:T.ty3 g c w u
we proved
∀g:G
.∀c:C
.∀w:T
.∀v:T
.∀x:T
.ty3 g c (THead (Flat Appl) w v) x
→(ex3_2
T
T
λu:T.λt0:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) x
λu:T.λt0:T.ty3 g c v (THead (Bind Abst) u t0)
λu:T.λ:T.ty3 g c w u)