DEFINITION ty3_shift1()
TYPE =
∀g:G.∀c:C.(wf3 g c c)→∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ty3 g (CSort (cbk c)) (app1 c t1) (app1 c t2))
BODY =
assume g: G
assume c: C
suppose H: wf3 g c c
assume y: C
suppose H0: wf3 g y c
we proceed by induction on H0 to prove (eq C y c)→∀t1:T.∀t2:T.(ty3 g y t1 t2)→(ty3 g (CSort (cbk y)) (app1 y t1) (app1 y t2))
case wf3_sort : m:nat ⇒
the thesis becomes
eq C (CSort m) (CSort m)
→∀t1:T.∀t2:T.∀H2:(ty3 g (CSort m) t1 t2).(ty3 g (CSort m) t1 t2)
suppose : eq C (CSort m) (CSort m)
assume t1: T
assume t2: T
suppose H2: ty3 g (CSort m) t1 t2
consider H2
we proved ty3 g (CSort m) t1 t2
that is equivalent to ty3 g (CSort (cbk (CSort m))) (app1 (CSort m) t1) (app1 (CSort m) t2)
eq C (CSort m) (CSort m)
→∀t1:T.∀t2:T.∀H2:(ty3 g (CSort m) t1 t2).(ty3 g (CSort m) t1 t2)
case wf3_bind : c1:C c2:C H1:wf3 g c1 c2 u:T t:T H3:ty3 g c1 u t b:B ⇒
the thesis becomes
∀H4:eq C (CHead c1 (Bind b) u) (CHead c2 (Bind b) u)
.∀t1:T
.∀t2:T
.∀H5:ty3 g (CHead c1 (Bind b) u) t1 t2
.ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
(H2) by induction hypothesis we know (eq C c1 c2)→∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→(ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2))
suppose H4: eq C (CHead c1 (Bind b) u) (CHead c2 (Bind b) u)
assume t1: T
assume t2: T
suppose H5: ty3 g (CHead c1 (Bind b) u) t1 t2
(H6)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c0 ⇒c0 (CHead c1 (Bind b) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c0 ⇒c0 (CHead c2 (Bind b) u)
end of H6
(H7)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
that is equivalent to eq C c1 c2
by (eq_ind_r . . . H2 . previous)
(eq C c1 c1)→∀t3:T.∀t4:T.(ty3 g c1 t3 t4)→(ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 t4))
end of H7
by (ty3_correct . . . . H5)
we proved ex T λt:T.ty3 g (CHead c1 (Bind b) u) t2 t
we proceed by induction on the previous result to prove
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
case ex_intro : x:T :ty3 g (CHead c1 (Bind b) u) t2 x ⇒
the thesis becomes
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
(h1)
by (refl_equal . .)
eq C c1 c1
end of h1
(h2)
by (ty3_bind . . . . H3 . . . H5)
ty3 g c1 (THead (Bind b) u t1) (THead (Bind b) u t2)
end of h2
by (H7 h1 . . h2)
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
we proved
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
that is equivalent to
ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2
∀H4:eq C (CHead c1 (Bind b) u) (CHead c2 (Bind b) u)
.∀t1:T
.∀t2:T
.∀H5:ty3 g (CHead c1 (Bind b) u) t1 t2
.ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind b) u t1)
app1 c1 (THead (Bind b) u t2)
case wf3_void : c1:C c2:C H1:wf3 g c1 c2 u:T H3:∀t:T.(ty3 g c1 u t)→False b:B ⇒
the thesis becomes
∀H4:eq C (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O))
.∀t1:T
.∀t2:T
.∀H5:ty3 g (CHead c1 (Bind b) u) t1 t2
.ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2
(H2) by induction hypothesis we know (eq C c1 c2)→∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→(ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2))
suppose H4: eq C (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O))
assume t1: T
assume t2: T
suppose H5: ty3 g (CHead c1 (Bind b) u) t1 t2
(H6)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind Void) (TSort O) OF CSort ⇒c1 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c0 ⇒c0 (CHead c1 (Bind b) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c1 | CHead c0 ⇒c0
CHead c2 (Bind Void) (TSort O)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
B
<λ:C.B>
CASE CHead c1 (Bind b) u OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:C.B>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
CHead c1 (Bind b) u
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
CHead c2 (Bind Void) (TSort O)
end of H7
(h1)
(H8)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind b) u OF CSort ⇒u | CHead t⇒t
<λ:C.T>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒u
| CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c1 (Bind b) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t
CHead c2 (Bind Void) (TSort O)
end of H8
suppose H9: eq B b Void
suppose H10: eq C c1 c2
(H11)
we proceed by induction on H9 to prove ty3 g (CHead c1 (Bind Void) u) t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H5
ty3 g (CHead c1 (Bind Void) u) t1 t2
end of H11
(H12)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind b) u OF CSort ⇒u | CHead t⇒t
<λ:C.T>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒u
| CHead t⇒t
that is equivalent to eq T u (TSort O)
we proceed by induction on the previous result to prove ty3 g (CHead c1 (Bind Void) (TSort O)) t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H11
ty3 g (CHead c1 (Bind Void) (TSort O)) t1 t2
end of H12
(h1)
(H14)
by (eq_ind_r . . . H2 . H10)
(eq C c1 c1)→∀t3:T.∀t4:T.(ty3 g c1 t3 t4)→(ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 t4))
end of H14
by (ty3_correct . . . . H12)
we proved ex T λt:T.ty3 g (CHead c1 (Bind Void) (TSort O)) t2 t
we proceed by induction on the previous result to prove
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind Void) (TSort O) t1)
app1 c1 (THead (Bind Void) (TSort O) t2)
case ex_intro : x:T :ty3 g (CHead c1 (Bind Void) (TSort O)) t2 x ⇒
the thesis becomes
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind Void) (TSort O) t1)
app1 c1 (THead (Bind Void) (TSort O) t2)
(h1)
by (refl_equal . .)
eq C c1 c1
end of h1
(h2)
by (ty3_sort . . .)
we proved ty3 g c1 (TSort O) (TSort (next g O))
by (ty3_bind . . . . previous . . . H12)
ty3
g
c1
THead (Bind Void) (TSort O) t1
THead (Bind Void) (TSort O) t2
end of h2
by (H14 h1 . . h2)
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind Void) (TSort O) t1)
app1 c1 (THead (Bind Void) (TSort O) t2)
we proved
ty3
g
CSort (cbk c1)
app1 c1 (THead (Bind Void) (TSort O) t1)
app1 c1 (THead (Bind Void) (TSort O) t2)
ty3
g
CSort (cbk (CHead c1 (Bind Void) (TSort O)))
app1 (CHead c1 (Bind Void) (TSort O)) t1
app1 (CHead c1 (Bind Void) (TSort O)) t2
end of h1
(h2)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind b) u OF CSort ⇒u | CHead t⇒t
<λ:C.T>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒u
| CHead t⇒t
eq T u (TSort O)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ty3
g
CSort (cbk (CHead c1 (Bind Void) u))
app1 (CHead c1 (Bind Void) u) t1
app1 (CHead c1 (Bind Void) u) t2
by (eq_ind_r . . . previous . H9)
we proved
ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2
eq B b Void
→(eq C c1 c2
→(ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2))
end of h1
(h2)
consider H7
we proved
eq
B
<λ:C.B>
CASE CHead c1 (Bind b) u OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:C.B>
CASE CHead c2 (Bind Void) (TSort O) OF
CSort ⇒b
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq B b Void
end of h2
by (h1 h2)
eq C c1 c2
→(ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind Void) (TSort O) OF CSort ⇒c1 | CHead c0 ⇒c0
eq C c1 c2
end of h2
by (h1 h2)
we proved
ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2
∀H4:eq C (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O))
.∀t1:T
.∀t2:T
.∀H5:ty3 g (CHead c1 (Bind b) u) t1 t2
.ty3
g
CSort (cbk (CHead c1 (Bind b) u))
app1 (CHead c1 (Bind b) u) t1
app1 (CHead c1 (Bind b) u) t2
case wf3_flat : c1:C c2:C H1:wf3 g c1 c2 u:T f:F ⇒
the thesis becomes
∀H3:eq C (CHead c1 (Flat f) u) c2
.∀t1:T
.∀t2:T
.ty3 g (CHead c1 (Flat f) u) t1 t2
→(ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2))
(H2) by induction hypothesis we know (eq C c1 c2)→∀t1:T.∀t2:T.(ty3 g c1 t1 t2)→(ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2))
suppose H3: eq C (CHead c1 (Flat f) u) c2
assume t1: T
assume t2: T
suppose : ty3 g (CHead c1 (Flat f) u) t1 t2
(H5)
by (f_equal . . . . . H3)
we proved eq C (CHead c1 (Flat f) u) c2
eq C (λe:C.e (CHead c1 (Flat f) u)) (λe:C.e c2)
end of H5
(H7)
by (eq_ind_r . . . H1 . H5)
wf3 g c1 (CHead c1 (Flat f) u)
end of H7
(H_x)
by (wf3_gen_head2 . . . . . H7)
ex B λb:B.eq K (Flat f) (Bind b)
end of H_x
(H8) consider H_x
we proceed by induction on H8 to prove
ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2)
case ex_intro : x:B H9:eq K (Flat f) (Bind x) ⇒
the thesis becomes
ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2)
(H10)
we proceed by induction on H9 to prove <λ:K.Prop> CASE Bind x OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
<λ:K.Prop> CASE Bind x OF Bind ⇒False | Flat ⇒True
end of H10
consider H10
we proved <λ:K.Prop> CASE Bind x OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2)
ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2)
we proved
ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2)
that is equivalent to
ty3
g
CSort (cbk (CHead c1 (Flat f) u))
app1 (CHead c1 (Flat f) u) t1
app1 (CHead c1 (Flat f) u) t2
∀H3:eq C (CHead c1 (Flat f) u) c2
.∀t1:T
.∀t2:T
.ty3 g (CHead c1 (Flat f) u) t1 t2
→(ty3
g
CSort (cbk c1)
app1 c1 (THead (Flat f) u t1)
app1 c1 (THead (Flat f) u t2))
we proved (eq C y c)→∀t1:T.∀t2:T.(ty3 g y t1 t2)→(ty3 g (CSort (cbk y)) (app1 y t1) (app1 y t2))
we proved
∀y:C
.wf3 g y c
→(eq C y c)→∀t1:T.∀t2:T.(ty3 g y t1 t2)→(ty3 g (CSort (cbk y)) (app1 y t1) (app1 y t2))
by (insert_eq . . . . previous H)
we proved ∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ty3 g (CSort (cbk c)) (app1 c t1) (app1 c t2))
we proved ∀g:G.∀c:C.(wf3 g c c)→∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ty3 g (CSort (cbk c)) (app1 c t1) (app1 c t2))