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