DEFINITION ty3_inference()
TYPE =
∀g:G.∀c:C.∀t1:T.(or (ex T λt2:T.ty3 g c t1 t2) ∀t2:T.(ty3 g c t1 t2)→False)
BODY =
assume g: G
assume c: C
assume t1: T
assume c2: C
assume t2: T
we proceed by induction on t2 to prove
∀c1:C.∀t3:T.(flt c1 t3 c2 t2)→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 t2 t3) ∀t3:T.(ty3 g c2 t2 t3)→False
case TSort : n:nat ⇒
the thesis becomes
∀c1:C.∀t3:T.(flt c1 t3 c2 (TSort n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 (TSort n) t3) ∀t3:T.(ty3 g c2 (TSort n) t3)→False
suppose : ∀c1:C.∀t3:T.(flt c1 t3 c2 (TSort n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
by (ty3_sort . . .)
we proved ty3 g c2 (TSort n) (TSort (next g n))
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (TSort n) t3
by (or_introl . . previous)
we proved or (ex T λt3:T.ty3 g c2 (TSort n) t3) ∀t3:T.(ty3 g c2 (TSort n) t3)→False
∀c1:C.∀t3:T.(flt c1 t3 c2 (TSort n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 (TSort n) t3) ∀t3:T.(ty3 g c2 (TSort n) t3)→False
case TLRef : n:nat ⇒
the thesis becomes
∀H:∀c1:C.∀t3:T.(flt c1 t3 c2 (TLRef n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
.or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
suppose H: ∀c1:C.∀t3:T.(flt c1 t3 c2 (TLRef n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
(H_x)
by (getl_dec . .)
or
ex_3 C B T λe:C.λb:B.λv:T.getl n c2 (CHead e (Bind b) v)
∀d:C.(getl n c2 d)→∀P:Prop.P
end of H_x
(H0) consider H_x
we proceed by induction on H0 to prove or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case or_introl : H1:ex_3 C B T λe:C.λb:B.λv:T.getl n c2 (CHead e (Bind b) v) ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
we proceed by induction on H1 to prove or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case ex_3_intro : x0:C x1:B x2:T H2:getl n c2 (CHead x0 (Bind x1) x2) ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
(H3)
by (getl_flt . . . . . H2)
we proved flt x0 x2 c2 (TLRef n)
by (H . . previous)
or (ex T λt4:T.ty3 g x0 x2 t4) ∀t4:T.(ty3 g x0 x2 t4)→False
end of H3
we proceed by induction on H3 to prove or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case or_introl : H4:ex T λt3:T.ty3 g x0 x2 t3 ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
we proceed by induction on H4 to prove or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case ex_intro : x:T H5:ty3 g x0 x2 x ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
suppose H6: getl n c2 (CHead x0 (Bind Abbr) x2)
by (ty3_abbr . . . . . H6 . H5)
we proved ty3 g c2 (TLRef n) (lift (S n) O x)
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (TLRef n) t3
by (or_introl . . previous)
we proved or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
getl n c2 (CHead x0 (Bind Abbr) x2)
→or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
suppose H6: getl n c2 (CHead x0 (Bind Abst) x2)
by (ty3_abst . . . . . H6 . H5)
we proved ty3 g c2 (TLRef n) (lift (S n) O x2)
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (TLRef n) t3
by (or_introl . . previous)
we proved or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
getl n c2 (CHead x0 (Bind Abst) x2)
→or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
suppose H6: getl n c2 (CHead x0 (Bind Void) x2)
assume t3: T
suppose H7: ty3 g c2 (TLRef n) t3
by (ty3_gen_lref . . . . H7)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3
λe:C.λu:T.λ:T.getl n c2 (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 c2 (lift (S n) O u) t3
λe:C.λu:T.λ:T.getl n c2 (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 False
case or_introl : H8:ex3_3 C T T λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abbr) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H8 to prove False
case ex3_3_intro : x3:C x4:T x5:T :pc3 c2 (lift (S n) O x5) t3 H10:getl n c2 (CHead x3 (Bind Abbr) x4) :ty3 g x3 x4 x5 ⇒
the thesis becomes False
(H13)
by (getl_mono . . . H6 . H10)
we proved eq C (CHead x0 (Bind Void) x2) (CHead x3 (Bind Abbr) x4)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x3 (Bind Abbr) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead x0 (Bind Void) x2 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead x0 (Bind Void) x2 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
<λ:C.Prop>
CASE CHead x3 (Bind Abbr) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
end of H13
consider H13
we proved
<λ:C.Prop>
CASE CHead x3 (Bind Abbr) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove False
False
False
case or_intror : H8:ex3_3 C T T λ:C.λu:T.λ:T.pc3 c2 (lift (S n) O u) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abst) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H8 to prove False
case ex3_3_intro : x3:C x4:T x5:T :pc3 c2 (lift (S n) O x4) t3 H10:getl n c2 (CHead x3 (Bind Abst) x4) :ty3 g x3 x4 x5 ⇒
the thesis becomes False
(H13)
by (getl_mono . . . H6 . H10)
we proved eq C (CHead x0 (Bind Void) x2) (CHead x3 (Bind Abst) x4)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead x3 (Bind Abst) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead x0 (Bind Void) x2 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead x0 (Bind Void) x2 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
<λ:C.Prop>
CASE CHead x3 (Bind Abst) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
end of H13
consider H13
we proved
<λ:C.Prop>
CASE CHead x3 (Bind Abst) x4 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove False
False
False
we proved False
we proved ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
by (or_intror . . previous)
we proved or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
getl n c2 (CHead x0 (Bind Void) x2)
→or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
by (previous . H2)
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case or_intror : H4:∀t3:T.(ty3 g x0 x2 t3)→False ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
assume t3: T
suppose H5: ty3 g c2 (TLRef n) t3
by (ty3_gen_lref . . . . H5)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3
λe:C.λu:T.λ:T.getl n c2 (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 c2 (lift (S n) O u) t3
λe:C.λu:T.λ:T.getl n c2 (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 False
case or_introl : H6:ex3_3 C T T λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abbr) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H6 to prove False
case ex3_3_intro : x3:C x4:T x5:T :pc3 c2 (lift (S n) O x5) t3 H8:getl n c2 (CHead x3 (Bind Abbr) x4) H9:ty3 g x3 x4 x5 ⇒
the thesis becomes False
(H10)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4)
we proceed by induction on the previous result to prove getl n c2 (CHead x3 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl n c2 (CHead x3 (Bind Abbr) x4)
end of H10
(H11)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x0 | CHead c0 ⇒c0
<λ:C.C> CASE CHead x3 (Bind Abbr) x4 OF CSort ⇒x0 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x0 | CHead c0 ⇒c0 (CHead x0 (Bind x1) x2)
λe:C.<λ:C.C> CASE e OF CSort ⇒x0 | CHead c0 ⇒c0 (CHead x3 (Bind Abbr) x4)
end of H11
(h1)
(H12)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead x0 (Bind x1) x2 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
<λ:C.B>
CASE CHead x3 (Bind Abbr) x4 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒x1 | CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
CHead x0 (Bind x1) x2
λe:C.<λ:C.B> CASE e OF CSort ⇒x1 | CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
CHead x3 (Bind Abbr) x4
end of H12
(h1)
(H13)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abbr) x4 OF CSort ⇒x2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x2 | CHead t⇒t (CHead x0 (Bind x1) x2)
λe:C.<λ:C.T> CASE e OF CSort ⇒x2 | CHead t⇒t (CHead x3 (Bind Abbr) x4)
end of H13
suppose : eq B x1 Abbr
suppose H15: eq C x0 x3
(H16)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abbr) x4 OF CSort ⇒x2 | CHead t⇒t
that is equivalent to eq T x2 x4
by (eq_ind_r . . . H10 . previous)
getl n c2 (CHead x3 (Bind Abbr) x2)
end of H16
(H17)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abbr) x4 OF CSort ⇒x2 | CHead t⇒t
that is equivalent to eq T x2 x4
by (eq_ind_r . . . H9 . previous)
ty3 g x3 x2 x5
end of H17
(H19)
by (eq_ind_r . . . H17 . H15)
ty3 g x0 x2 x5
end of H19
by (H4 . H19)
we proved False
(eq B x1 Abbr)→(eq C x0 x3)→False
end of h1
(h2)
consider H12
we proved
eq
B
<λ:C.B>
CASE CHead x0 (Bind x1) x2 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
<λ:C.B>
CASE CHead x3 (Bind Abbr) x4 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
eq B x1 Abbr
end of h2
by (h1 h2)
(eq C x0 x3)→False
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x0 | CHead c0 ⇒c0
<λ:C.C> CASE CHead x3 (Bind Abbr) x4 OF CSort ⇒x0 | CHead c0 ⇒c0
eq C x0 x3
end of h2
by (h1 h2)
False
False
case or_intror : H6:ex3_3 C T T λ:C.λu:T.λ:T.pc3 c2 (lift (S n) O u) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abst) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H6 to prove False
case ex3_3_intro : x3:C x4:T x5:T H7:pc3 c2 (lift (S n) O x4) t3 H8:getl n c2 (CHead x3 (Bind Abst) x4) H9:ty3 g x3 x4 x5 ⇒
the thesis becomes False
(H10)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4)
we proceed by induction on the previous result to prove getl n c2 (CHead x3 (Bind Abst) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl n c2 (CHead x3 (Bind Abst) x4)
end of H10
(H11)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x0 | CHead c0 ⇒c0
<λ:C.C> CASE CHead x3 (Bind Abst) x4 OF CSort ⇒x0 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x0 | CHead c0 ⇒c0 (CHead x0 (Bind x1) x2)
λe:C.<λ:C.C> CASE e OF CSort ⇒x0 | CHead c0 ⇒c0 (CHead x3 (Bind Abst) x4)
end of H11
(h1)
(H12)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead x0 (Bind x1) x2 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
<λ:C.B>
CASE CHead x3 (Bind Abst) x4 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒x1 | CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
CHead x0 (Bind x1) x2
λe:C.<λ:C.B> CASE e OF CSort ⇒x1 | CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
CHead x3 (Bind Abst) x4
end of H12
(h1)
(H13)
by (getl_mono . . . H2 . H8)
we proved eq C (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abst) x4 OF CSort ⇒x2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x2 | CHead t⇒t (CHead x0 (Bind x1) x2)
λe:C.<λ:C.T> CASE e OF CSort ⇒x2 | CHead t⇒t (CHead x3 (Bind Abst) x4)
end of H13
suppose : eq B x1 Abst
suppose H15: eq C x0 x3
(H16)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abst) x4 OF CSort ⇒x2 | CHead t⇒t
that is equivalent to eq T x2 x4
by (eq_ind_r . . . H10 . previous)
getl n c2 (CHead x3 (Bind Abst) x2)
end of H16
(H17)
consider H13
we proved
eq
T
<λ:C.T> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x2 | CHead t⇒t
<λ:C.T> CASE CHead x3 (Bind Abst) x4 OF CSort ⇒x2 | CHead t⇒t
that is equivalent to eq T x2 x4
by (eq_ind_r . . . H9 . previous)
ty3 g x3 x2 x5
end of H17
(H20)
by (eq_ind_r . . . H17 . H15)
ty3 g x0 x2 x5
end of H20
by (H4 . H20)
we proved False
(eq B x1 Abst)→(eq C x0 x3)→False
end of h1
(h2)
consider H12
we proved
eq
B
<λ:C.B>
CASE CHead x0 (Bind x1) x2 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
<λ:C.B>
CASE CHead x3 (Bind Abst) x4 OF
CSort ⇒x1
| CHead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x1
eq B x1 Abst
end of h2
by (h1 h2)
(eq C x0 x3)→False
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead x0 (Bind x1) x2 OF CSort ⇒x0 | CHead c0 ⇒c0
<λ:C.C> CASE CHead x3 (Bind Abst) x4 OF CSort ⇒x0 | CHead c0 ⇒c0
eq C x0 x3
end of h2
by (h1 h2)
False
False
we proved False
we proved ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
by (or_intror . . previous)
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case or_intror : H1:∀d:C.(getl n c2 d)→∀P:Prop.P ⇒
the thesis becomes or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
assume t3: T
suppose H2: ty3 g c2 (TLRef n) t3
by (ty3_gen_lref . . . . H2)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3
λe:C.λu:T.λ:T.getl n c2 (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 c2 (lift (S n) O u) t3
λe:C.λu:T.λ:T.getl n c2 (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 False
case or_introl : H3:ex3_3 C T T λ:C.λ:T.λt:T.pc3 c2 (lift (S n) O t) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abbr) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H3 to prove False
case ex3_3_intro : x0:C x1:T x2:T :pc3 c2 (lift (S n) O x2) t3 H5:getl n c2 (CHead x0 (Bind Abbr) x1) :ty3 g x0 x1 x2 ⇒
the thesis becomes False
by (H1 . H5 .)
False
False
case or_intror : H3:ex3_3 C T T λ:C.λu:T.λ:T.pc3 c2 (lift (S n) O u) t3 λe:C.λu:T.λ:T.getl n c2 (CHead e (Bind Abst) u) λe:C.λu:T.λt:T.ty3 g e u t ⇒
the thesis becomes False
we proceed by induction on H3 to prove False
case ex3_3_intro : x0:C x1:T x2:T :pc3 c2 (lift (S n) O x1) t3 H5:getl n c2 (CHead x0 (Bind Abst) x1) :ty3 g x0 x1 x2 ⇒
the thesis becomes False
by (H1 . H5 .)
False
False
we proved False
we proved ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
by (or_intror . . previous)
or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
we proved or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
∀H:∀c1:C.∀t3:T.(flt c1 t3 c2 (TLRef n))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
.or (ex T λt3:T.ty3 g c2 (TLRef n) t3) ∀t3:T.(ty3 g c2 (TLRef n) t3)→False
case THead : k:K t:T t0:T ⇒
the thesis becomes
∀H1:∀c1:C.∀t3:T.(flt c1 t3 c2 (THead k t t0))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
.or (ex T λt3:T.ty3 g c2 (THead k t t0) t3) ∀t3:T.(ty3 g c2 (THead k t t0) t3)→False
() by induction hypothesis we know
∀c1:C.∀t3:T.(flt c1 t3 c2 t)→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 t t3) ∀t3:T.(ty3 g c2 t t3)→False
() by induction hypothesis we know
∀c1:C.∀t3:T.(flt c1 t3 c2 t0)→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 t0 t3) ∀t3:T.(ty3 g c2 t0 t3)→False
suppose H1: ∀c1:C.∀t3:T.(flt c1 t3 c2 (THead k t t0))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
assume b: B
suppose H2:
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Bind b) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
(H3)
by (flt_thead_sx . . . .)
we proved flt c2 t c2 (THead (Bind b) t t0)
by (H2 . . previous)
or (ex T λt4:T.ty3 g c2 t t4) ∀t4:T.(ty3 g c2 t t4)→False
end of H3
we proceed by induction on H3 to prove
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case or_introl : H4:ex T λt3:T.ty3 g c2 t t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
we proceed by induction on H4 to prove
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case ex_intro : x:T H5:ty3 g c2 t x ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
(H6)
by (flt_shift . . . .)
we proved flt (CHead c2 (Bind b) t) t0 c2 (THead (Bind b) t t0)
by (H2 . . previous)
or
ex T λt4:T.ty3 g (CHead c2 (Bind b) t) t0 t4
∀t4:T.(ty3 g (CHead c2 (Bind b) t) t0 t4)→False
end of H6
we proceed by induction on H6 to prove
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case or_introl : H7:ex T λt3:T.ty3 g (CHead c2 (Bind b) t) t0 t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
we proceed by induction on H7 to prove
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case ex_intro : x0:T H8:ty3 g (CHead c2 (Bind b) t) t0 x0 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
by (ty3_bind . . . . H5 . . . H8)
we proved ty3 g c2 (THead (Bind b) t t0) (THead (Bind b) t x0)
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
by (or_introl . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case or_intror : H7:∀t3:T.(ty3 g (CHead c2 (Bind b) t) t0 t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
assume t3: T
suppose H8: ty3 g c2 (THead (Bind b) t t0) t3
by (ty3_gen_bind . . . . . . H8)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind b) t t2) t3
λ:T.λt:T.ty3 g c2 t t
λt2:T.λ:T.ty3 g (CHead c2 (Bind b) t) t0 t2
we proceed by induction on the previous result to prove False
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Bind b) t x0) t3 :ty3 g c2 t x1 H11:ty3 g (CHead c2 (Bind b) t) t0 x0 ⇒
the thesis becomes False
by (H7 . H11)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
case or_intror : H4:∀t3:T.(ty3 g c2 t t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
assume t3: T
suppose H5: ty3 g c2 (THead (Bind b) t t0) t3
by (ty3_gen_bind . . . . . . H5)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c2 (THead (Bind b) t t2) t3
λ:T.λt:T.ty3 g c2 t t
λt2:T.λ:T.ty3 g (CHead c2 (Bind b) t) t0 t2
we proceed by induction on the previous result to prove False
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Bind b) t x0) t3 H7:ty3 g c2 t x1 :ty3 g (CHead c2 (Bind b) t) t0 x0 ⇒
the thesis becomes False
by (H4 . H7)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
we proved
or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
∀H2:∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Bind b) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
.or
ex T λt3:T.ty3 g c2 (THead (Bind b) t t0) t3
∀t3:T.(ty3 g c2 (THead (Bind b) t t0) t3)→False
assume f: F
suppose H2:
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat f) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
suppose H3:
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat Appl) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
(H4)
by (flt_thead_sx . . . .)
we proved flt c2 t c2 (THead (Flat Appl) t t0)
by (H3 . . previous)
or (ex T λt4:T.ty3 g c2 t t4) ∀t4:T.(ty3 g c2 t t4)→False
end of H4
we proceed by induction on H4 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_introl : H5:ex T λt3:T.ty3 g c2 t t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
we proceed by induction on H5 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex_intro : x:T H6:ty3 g c2 t x ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
(H7)
by (flt_thead_dx . . . .)
we proved flt c2 t0 c2 (THead (Flat Appl) t t0)
by (H3 . . previous)
or (ex T λt4:T.ty3 g c2 t0 t4) ∀t4:T.(ty3 g c2 t0 t4)→False
end of H7
we proceed by induction on H7 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_introl : H8:ex T λt3:T.ty3 g c2 t0 t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
we proceed by induction on H8 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex_intro : x0:T H9:ty3 g c2 t0 x0 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
by (ty3_correct . . . . H9)
we proved ex T λt:T.ty3 g c2 x0 t
we proceed by induction on the previous result to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex_intro : x1:T H10:ty3 g c2 x0 x1 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
by (ty3_correct . . . . H6)
we proved ex T λt:T.ty3 g c2 x t
we proceed by induction on the previous result to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex_intro : x2:T H11:ty3 g c2 x x2 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
(H12) by (ty3_sn3 . . . . H11) we proved sn3 c2 x
(H_x)
by (nf2_sn3 . . H12)
ex2 T λu:T.pr3 c2 x u λu:T.nf2 c2 u
end of H_x
(H13) consider H_x
we proceed by induction on H13 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex_intro2 : x3:T H14:pr3 c2 x x3 H15:nf2 c2 x3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
(H16) by (ty3_sred_pr3 . . . H14 . . H11) we proved ty3 g c2 x3 x2
(H_x0)
by (pc3_abst_dec . . . . H10 . . H16)
or
ex4_2
T
T
λu:T.λ:T.pc3 c2 x0 (THead (Bind Abst) x3 u)
λu:T.λv2:T.ty3 g c2 (THead (Bind Abst) v2 u) x1
λ:T.λv2:T.pr3 c2 x3 v2
λ:T.λv2:T.nf2 c2 v2
∀u:T.(pc3 c2 x0 (THead (Bind Abst) x3 u))→False
end of H_x0
(H17) consider H_x0
we proceed by induction on H17 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_introl : H18:ex4_2 T T λu:T.λ:T.pc3 c2 x0 (THead (Bind Abst) x3 u) λu:T.λv2:T.ty3 g c2 (THead (Bind Abst) v2 u) x1 λ:T.λv2:T.pr3 c2 x3 v2 λ:T.λv2:T.nf2 c2 v2 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
we proceed by induction on H18 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case ex4_2_intro : x4:T x5:T H19:pc3 c2 x0 (THead (Bind Abst) x3 x4) H20:ty3 g c2 (THead (Bind Abst) x5 x4) x1 H21:pr3 c2 x3 x5 :nf2 c2 x5 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
(H_y)
by (nf2_pr3_unfold . . . H21 H15)
eq T x3 x5
end of H_y
(H24)
by (eq_ind_r . . . H20 . H_y)
ty3 g c2 (THead (Bind Abst) x3 x4) x1
end of H24
(h1)
by (ty3_tred . . . . H6 . H14)
ty3 g c2 t x3
end of h1
(h2)
by (ty3_conv . . . . H24 . . H9 H19)
ty3 g c2 t0 (THead (Bind Abst) x3 x4)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
c2
THead (Flat Appl) t t0
THead (Flat Appl) t (THead (Bind Abst) x3 x4)
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
by (or_introl . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_intror : H18:∀u:T.(pc3 c2 x0 (THead (Bind Abst) x3 u))→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
assume t3: T
suppose H19: ty3 g c2 (THead (Flat Appl) t t0) t3
by (ty3_gen_appl . . . . . H19)
we proved
ex3_2
T
T
λu:T.λt:T.pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) u t)) t3
λu:T.λt:T.ty3 g c2 t0 (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c2 t u
we proceed by induction on the previous result to prove False
case ex3_2_intro : x4:T x5:T :pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) x4 x5)) t3 H21:ty3 g c2 t0 (THead (Bind Abst) x4 x5) H22:ty3 g c2 t x4 ⇒
the thesis becomes False
(H_y)
by (ty3_unique . . . . H22 . H6)
pc3 c2 x4 x
end of H_y
(H_y0)
by (ty3_unique . . . . H21 . H9)
pc3 c2 (THead (Bind Abst) x4 x5) x0
end of H_y0
(h1)
by (pc3_s . . . H_y0)
pc3 c2 x0 (THead (Bind Abst) x4 x5)
end of h1
(h2)
by (pc3_pr3_r . . . H14)
we proved pc3 c2 x x3
by (pc3_t . . . H_y . previous)
we proved pc3 c2 x4 x3
by (pc3_head_1 . . . previous . .)
pc3 c2 (THead (Bind Abst) x4 x5) (THead (Bind Abst) x3 x5)
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c2 x0 (THead (Bind Abst) x3 x5)
by (H18 . previous)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_intror : H8:∀t3:T.(ty3 g c2 t0 t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
assume t3: T
suppose H9: ty3 g c2 (THead (Flat Appl) t t0) t3
by (ty3_gen_appl . . . . . H9)
we proved
ex3_2
T
T
λu:T.λt:T.pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) u t)) t3
λu:T.λt:T.ty3 g c2 t0 (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c2 t u
we proceed by induction on the previous result to prove False
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) x0 x1)) t3 H11:ty3 g c2 t0 (THead (Bind Abst) x0 x1) :ty3 g c2 t x0 ⇒
the thesis becomes False
by (H8 . H11)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
case or_intror : H5:∀t3:T.(ty3 g c2 t t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
assume t3: T
suppose H6: ty3 g c2 (THead (Flat Appl) t t0) t3
by (ty3_gen_appl . . . . . H6)
we proved
ex3_2
T
T
λu:T.λt:T.pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) u t)) t3
λu:T.λt:T.ty3 g c2 t0 (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c2 t u
we proceed by induction on the previous result to prove False
case ex3_2_intro : x0:T x1:T :pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) x0 x1)) t3 :ty3 g c2 t0 (THead (Bind Abst) x0 x1) H9:ty3 g c2 t x0 ⇒
the thesis becomes False
by (H5 . H9)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
we proved
or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat Appl) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
→(or
ex T λt3:T.ty3 g c2 (THead (Flat Appl) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Appl) t t0) t3)→False)
suppose H3:
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat Cast) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
(H4)
by (flt_thead_sx . . . .)
we proved flt c2 t c2 (THead (Flat Cast) t t0)
by (H3 . . previous)
or (ex T λt4:T.ty3 g c2 t t4) ∀t4:T.(ty3 g c2 t t4)→False
end of H4
we proceed by induction on H4 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_introl : H5:ex T λt3:T.ty3 g c2 t t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
we proceed by induction on H5 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case ex_intro : x:T H6:ty3 g c2 t x ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
(H7)
by (flt_thead_dx . . . .)
we proved flt c2 t0 c2 (THead (Flat Cast) t t0)
by (H3 . . previous)
or (ex T λt4:T.ty3 g c2 t0 t4) ∀t4:T.(ty3 g c2 t0 t4)→False
end of H7
we proceed by induction on H7 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_introl : H8:ex T λt3:T.ty3 g c2 t0 t3 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
we proceed by induction on H8 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case ex_intro : x0:T H9:ty3 g c2 t0 x0 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
by (ty3_correct . . . . H9)
we proved ex T λt:T.ty3 g c2 x0 t
we proceed by induction on the previous result to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case ex_intro : x1:T H10:ty3 g c2 x0 x1 ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
(H_x)
by (pc3_dec . . . . H10 . . H6)
or (pc3 c2 x0 t) (pc3 c2 x0 t)→False
end of H_x
(H11) consider H_x
we proceed by induction on H11 to prove
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_introl : H12:pc3 c2 x0 t ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
by (ty3_conv . . . . H6 . . H9 H12)
we proved ty3 g c2 t0 t
by (ty3_cast . . . . previous . H6)
we proved ty3 g c2 (THead (Flat Cast) t t0) (THead (Flat Cast) x t)
by (ex_intro . . . previous)
we proved ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
by (or_introl . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_intror : H12:(pc3 c2 x0 t)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
assume t3: T
suppose H13: ty3 g c2 (THead (Flat Cast) t t0) t3
by (ty3_gen_cast . . . . . H13)
we proved ex3 T λt0:T.pc3 c2 (THead (Flat Cast) t0 t) t3 λ:T.ty3 g c2 t0 t λt0:T.ty3 g c2 t t0
we proceed by induction on the previous result to prove False
case ex3_intro : x2:T :pc3 c2 (THead (Flat Cast) x2 t) t3 H15:ty3 g c2 t0 t H16:ty3 g c2 t x2 ⇒
the thesis becomes False
(H_y0)
by (ty3_unique . . . . H15 . H9)
pc3 c2 t x0
end of H_y0
consider H_y0
we proved pc3 c2 t x0
that is equivalent to ex2 T λx:T.pr3 c2 t x λx:T.pr3 c2 x0 x
by (ex2_sym . . . previous)
we proved ex2 T λx:T.pr3 c2 x0 x λx:T.pr3 c2 t x
that is equivalent to pc3 c2 x0 t
by (H12 previous)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_intror : H8:∀t3:T.(ty3 g c2 t0 t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
assume t3: T
suppose H9: ty3 g c2 (THead (Flat Cast) t t0) t3
by (ty3_gen_cast . . . . . H9)
we proved ex3 T λt0:T.pc3 c2 (THead (Flat Cast) t0 t) t3 λ:T.ty3 g c2 t0 t λt0:T.ty3 g c2 t t0
we proceed by induction on the previous result to prove False
case ex3_intro : x0:T :pc3 c2 (THead (Flat Cast) x0 t) t3 H11:ty3 g c2 t0 t :ty3 g c2 t x0 ⇒
the thesis becomes False
by (H8 . H11)
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
case or_intror : H5:∀t3:T.(ty3 g c2 t t3)→False ⇒
the thesis becomes
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
assume t3: T
suppose H6: ty3 g c2 (THead (Flat Cast) t t0) t3
by (ty3_gen_cast . . . . . H6)
we proved ex3 T λt0:T.pc3 c2 (THead (Flat Cast) t0 t) t3 λ:T.ty3 g c2 t0 t λt0:T.ty3 g c2 t t0
we proceed by induction on the previous result to prove False
case ex3_intro : x0:T :pc3 c2 (THead (Flat Cast) x0 t) t3 :ty3 g c2 t0 t H9:ty3 g c2 t x0 ⇒
the thesis becomes False
by (ty3_correct . . . . H9)
we proved ex T λt:T.ty3 g c2 x0 t
we proceed by induction on the previous result to prove False
case ex_intro : x:T :ty3 g c2 x0 x ⇒
the thesis becomes False
by (H5 . H9)
False
False
we proved False
we proved ∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
by (or_intror . . previous)
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
we proved
or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False
∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat Cast) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
→(or
ex T λt3:T.ty3 g c2 (THead (Flat Cast) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat Cast) t t0) t3)→False)
by (previous . H2)
we proved
or
ex T λt3:T.ty3 g c2 (THead (Flat f) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat f) t t0) t3)→False
∀H2:∀c1:C
.∀t3:T
.flt c1 t3 c2 (THead (Flat f) t t0)
→or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False
.or
ex T λt3:T.ty3 g c2 (THead (Flat f) t t0) t3
∀t3:T.(ty3 g c2 (THead (Flat f) t t0) t3)→False
by (previous . H1)
we proved or (ex T λt3:T.ty3 g c2 (THead k t t0) t3) ∀t3:T.(ty3 g c2 (THead k t t0) t3)→False
∀H1:∀c1:C.∀t3:T.(flt c1 t3 c2 (THead k t t0))→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
.or (ex T λt3:T.ty3 g c2 (THead k t t0) t3) ∀t3:T.(ty3 g c2 (THead k t t0) t3)→False
we proved
∀c1:C.∀t3:T.(flt c1 t3 c2 t2)→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 t2 t3) ∀t3:T.(ty3 g c2 t2 t3)→False
we proved
∀c2:C
.∀t2:T
.∀c1:C.∀t3:T.(flt c1 t3 c2 t2)→(or (ex T λt4:T.ty3 g c1 t3 t4) ∀t4:T.(ty3 g c1 t3 t4)→False)
→or (ex T λt3:T.ty3 g c2 t2 t3) ∀t3:T.(ty3 g c2 t2 t3)→False
by (flt_wf_ind . previous . .)
we proved or (ex T λt2:T.ty3 g c t1 t2) ∀t2:T.(ty3 g c t1 t2)→False
we proved ∀g:G.∀c:C.∀t1:T.(or (ex T λt2:T.ty3 g c t1 t2) ∀t2:T.(ty3 g c t1 t2)→False)