DEFINITION ex1_ty3()
TYPE =
∀g:G.∀u:T.(ty3 g ex1_c ex1_t u)→∀P:Prop.P
BODY =
assume g: G
assume u: T
we must prove (ty3 g ex1_c ex1_t u)→∀P:Prop.P
or equivalently
(ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead
Flat Appl
TLRef O
THead (Bind Abst) (TLRef (S (S O))) (TSort O)
u)
→∀P:Prop.P
suppose H:
ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead
Flat Appl
TLRef O
THead (Bind Abst) (TLRef (S (S O))) (TSort O)
u
assume P: Prop
by (ty3_gen_appl . . . . . H)
we proved
ex3_2
T
T
λu:T
.λt:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead (Flat Appl) (TLRef O) (THead (Bind Abst) u t)
u
λu:T
.λt:T
.ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead (Bind Abst) (TLRef (S (S O))) (TSort O)
THead (Bind Abst) u t
λu:T
.λ:T
.ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef O
u
we proceed by induction on the previous result to prove P
case ex3_2_intro : x0:T x1:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) x0 x1)) u H1:ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) (THead (Bind Abst) x0 x1) H2:ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef O) x0 ⇒
the thesis becomes P
by (ty3_gen_lref . . . . H2)
we proved
or
ex3_3
C
T
T
λ:C
.λ:T
.λt:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O t
x0
λe:C
.λu:T
.λ:T
.getl
O
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O u
x0
λe:C
.λu:T
.λ:T
.getl
O
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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 P
case or_introl : H3:ex3_3 C T T λ:C.λ:T.λt:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O t) x0 λe:C.λu0:T.λ:T.getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H3 to prove P
case ex3_3_intro : x2:C x3:T x4:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O x4) x0 H5:getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) :ty3 g x2 x3 x4 ⇒
the thesis becomes P
by (ty3_gen_bind . . . . . . H1)
we proved
ex3_2
T
T
λt2:T
.λ:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead (Bind Abst) (TLRef (S (S O))) t2
THead (Bind Abst) x0 x1
λ:T
.λt:T
.ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
t
λt2:T
.λ:T
.ty3
g
CHead
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
Bind Abst
TLRef (S (S O))
TSort O
t2
we proceed by induction on the previous result to prove P
case ex3_2_intro : x5:T x6:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 x1) H8:ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x6 :ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) x5 ⇒
the thesis becomes P
by (ty3_gen_lref . . . . H8)
we proved
or
ex3_3
C
T
T
λ:C
.λ:T
.λt:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S (S (S O))) O t
x6
λe:C
.λu:T
.λ:T
.getl
S (S O)
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S (S (S O))) O u
x6
λe:C
.λu:T
.λ:T
.getl
S (S O)
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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 P
case or_introl : H10:ex3_3 C T T λ:C.λ:T.λt:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6 λe:C.λu0:T.λ:T.getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H10 to prove P
case ex3_3_intro : x7:C x8:T x9:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x9) x6 H12:getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 (Bind Abbr) x8) :ty3 g x7 x8 x9 ⇒
the thesis becomes P
(H14)
by (getl_gen_S . . . . . H12)
we proved
getl
r (Bind Abst) (S O)
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x7 (Bind Abbr) x8
by (getl_gen_all . . . previous)
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
end of H14
consider H14
we proved
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
that is equivalent to
ex2
C
λe:C
.drop
S O
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
we proceed by induction on the previous result to prove P
case ex_intro2 : x:C :drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x :clear x (CHead x7 (Bind Abbr) x8) ⇒
the thesis becomes P
(H17)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abbr) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abbr) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 x2 (Bind Abbr) x3 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 x2 (Bind Abbr) x3 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
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 H17
consider H17
we proved
<λ:C.Prop>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 P
P
P
P
case or_intror : H10:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6 λe:C.λu0:T.λ:T.getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H10 to prove P
case ex3_3_intro : x7:C x8:T x9:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x8) x6 H12:getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 (Bind Abst) x8) :ty3 g x7 x8 x9 ⇒
the thesis becomes P
(H14)
by (getl_gen_S . . . . . H12)
we proved
getl
r (Bind Abst) (S O)
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x7 (Bind Abst) x8
by (getl_gen_all . . . previous)
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
end of H14
consider H14
we proved
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
that is equivalent to
ex2
C
λe:C
.drop
S O
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
we proceed by induction on the previous result to prove P
case ex_intro2 : x:C :drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x :clear x (CHead x7 (Bind Abst) x8) ⇒
the thesis becomes P
(H17)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abbr) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abbr) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 x2 (Bind Abbr) x3 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 x2 (Bind Abbr) x3 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
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 H17
consider H17
we proved
<λ:C.Prop>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O 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 P
P
P
P
P
P
P
case or_intror : H3:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0 λe:C.λu0:T.λ:T.getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H3 to prove P
case ex3_3_intro : x2:C x3:T x4:T H4:pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O x3) x0 H5:getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H6:ty3 g x2 x3 x4 ⇒
the thesis becomes P
by (ty3_gen_bind . . . . . . H1)
we proved
ex3_2
T
T
λt2:T
.λ:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead (Bind Abst) (TLRef (S (S O))) t2
THead (Bind Abst) x0 x1
λ:T
.λt:T
.ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
t
λt2:T
.λ:T
.ty3
g
CHead
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
Bind Abst
TLRef (S (S O))
TSort O
t2
we proceed by induction on the previous result to prove P
case ex3_2_intro : x5:T x6:T H7:pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 x1) H8:ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x6 :ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) x5 ⇒
the thesis becomes P
by (ty3_gen_lref . . . . H8)
we proved
or
ex3_3
C
T
T
λ:C
.λ:T
.λt:T
.pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S (S (S O))) O t
x6
λe:C
.λu:T
.λ:T
.getl
S (S O)
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S (S (S O))) O u
x6
λe:C
.λu:T
.λ:T
.getl
S (S O)
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
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 P
case or_introl : H10:ex3_3 C T T λ:C.λ:T.λt:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6 λe:C.λu0:T.λ:T.getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H10 to prove P
case ex3_3_intro : x7:C x8:T x9:T :pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x9) x6 H12:getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 (Bind Abbr) x8) :ty3 g x7 x8 x9 ⇒
the thesis becomes P
(H14)
by (getl_gen_S . . . . . H12)
we proved
getl
r (Bind Abst) (S O)
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x7 (Bind Abbr) x8
by (getl_gen_all . . . previous)
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
end of H14
consider H14
we proved
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
that is equivalent to
ex2
C
λe:C
.drop
S O
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abbr) x8)
we proceed by induction on the previous result to prove P
case ex_intro2 : x:C H15:drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x H16:clear x (CHead x7 (Bind Abbr) x8) ⇒
the thesis becomes P
(H17)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abst) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abst) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x2 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x2
| CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x2 | CHead c ⇒c (CHead x2 (Bind Abst) x3)
λe:C.<λ:C.C> CASE e OF CSort ⇒x2 | CHead c ⇒c
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
end of H17
(h1)
(H18)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abst) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abst) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x3 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x3
| CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x3 | CHead t⇒t (CHead x2 (Bind Abst) x3)
λe:C.<λ:C.T> CASE e OF CSort ⇒x3 | CHead t⇒t
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
end of H18
suppose H19:
eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
(H20)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x3 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x3
| CHead t⇒t
that is equivalent to eq T x3 (TLRef O)
we proceed by induction on the previous result to prove ty3 g x2 (TLRef O) x4
case refl_equal : ⇒
the thesis becomes the hypothesis H6
ty3 g x2 (TLRef O) x4
end of H20
(H23)
by (drop_gen_drop . . . . . H15)
we proved
drop
r (Bind Abst) O
O
CHead (CSort O) (Bind Abst) (TSort O)
x
that is equivalent to drop O O (CHead (CSort O) (Bind Abst) (TSort O)) x
by (drop_gen_refl . . previous)
we proved eq C (CHead (CSort O) (Bind Abst) (TSort O)) x
by (eq_ind_r . . . H16 . previous)
clear
CHead (CSort O) (Bind Abst) (TSort O)
CHead x7 (Bind Abbr) x8
end of H23
(H24)
by (clear_gen_bind . . . . H23)
we proved
eq
C
CHead x7 (Bind Abbr) x8
CHead (CSort O) (Bind Abst) (TSort O)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead (CSort O) (Bind Abst) (TSort O) 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 x7 (Bind Abbr) x8 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 x7 (Bind Abbr) x8 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 (CSort O) (Bind Abst) (TSort O) 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 H24
consider H24
we proved
<λ:C.Prop>
CASE CHead (CSort O) (Bind Abst) (TSort O) 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 P
we proved P
(eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O)
→P
end of h1
(h2)
consider H17
we proved
eq
C
<λ:C.C> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x2 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x2
| CHead c ⇒c
eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
end of h2
by (h1 h2)
P
P
P
case or_intror : H10:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6 λe:C.λu0:T.λ:T.getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H10 to prove P
case ex3_3_intro : x7:C x8:T x9:T H11:pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x8) x6 H12:getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 (Bind Abst) x8) H13:ty3 g x7 x8 x9 ⇒
the thesis becomes P
(H14)
by (getl_gen_S . . . . . H12)
we proved
getl
r (Bind Abst) (S O)
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x7 (Bind Abst) x8
by (getl_gen_all . . . previous)
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
end of H14
consider H14
we proved
ex2
C
λe:C
.drop
r (Bind Abst) (S O)
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
that is equivalent to
ex2
C
λe:C
.drop
S O
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
e
λe:C.clear e (CHead x7 (Bind Abst) x8)
we proceed by induction on the previous result to prove P
case ex_intro2 : x:C H15:drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x H16:clear x (CHead x7 (Bind Abst) x8) ⇒
the thesis becomes P
(H17)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abst) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abst) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x2 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x2
| CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x2 | CHead c ⇒c (CHead x2 (Bind Abst) x3)
λe:C.<λ:C.C> CASE e OF CSort ⇒x2 | CHead c ⇒c
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
end of H17
(h1)
(H18)
by (getl_gen_O . . H5)
we proved
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead x2 (Bind Abst) x3
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x2 (Bind Abst) x3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x3 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x3
| CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x3 | CHead t⇒t (CHead x2 (Bind Abst) x3)
λe:C.<λ:C.T> CASE e OF CSort ⇒x3 | CHead t⇒t
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
end of H18
suppose H19:
eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
(H20)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x3 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x3
| CHead t⇒t
that is equivalent to eq T x3 (TLRef O)
we proceed by induction on the previous result to prove ty3 g x2 (TLRef O) x4
case refl_equal : ⇒
the thesis becomes the hypothesis H6
ty3 g x2 (TLRef O) x4
end of H20
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x3 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x3
| CHead t⇒t
that is equivalent to eq T x3 (TLRef O)
we proceed by induction on the previous result to prove
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O (TLRef O)
x0
case refl_equal : ⇒
the thesis becomes the hypothesis H4
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O (TLRef O)
x0
end of H21
(H22)
we proceed by induction on H19 to prove
ty3
g
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
TLRef O
x4
case refl_equal : ⇒
the thesis becomes the hypothesis H20
ty3
g
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
TLRef O
x4
end of H22
(H23)
by (drop_gen_drop . . . . . H15)
we proved
drop
r (Bind Abst) O
O
CHead (CSort O) (Bind Abst) (TSort O)
x
that is equivalent to drop O O (CHead (CSort O) (Bind Abst) (TSort O)) x
by (drop_gen_refl . . previous)
we proved eq C (CHead (CSort O) (Bind Abst) (TSort O)) x
by (eq_ind_r . . . H16 . previous)
clear
CHead (CSort O) (Bind Abst) (TSort O)
CHead x7 (Bind Abst) x8
end of H23
(H24)
by (clear_gen_bind . . . . H23)
we proved
eq
C
CHead x7 (Bind Abst) x8
CHead (CSort O) (Bind Abst) (TSort O)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x7 (Bind Abst) x8 OF CSort ⇒x7 | CHead c ⇒c
<λ:C.C>
CASE CHead (CSort O) (Bind Abst) (TSort O) OF
CSort ⇒x7
| CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x7 | CHead c ⇒c (CHead x7 (Bind Abst) x8)
λe:C.<λ:C.C> CASE e OF CSort ⇒x7 | CHead c ⇒c
CHead (CSort O) (Bind Abst) (TSort O)
end of H24
(h1)
(H25)
by (clear_gen_bind . . . . H23)
we proved
eq
C
CHead x7 (Bind Abst) x8
CHead (CSort O) (Bind Abst) (TSort O)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x7 (Bind Abst) x8 OF CSort ⇒x8 | CHead t⇒t
<λ:C.T>
CASE CHead (CSort O) (Bind Abst) (TSort O) OF
CSort ⇒x8
| CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x8 | CHead t⇒t (CHead x7 (Bind Abst) x8)
λe:C.<λ:C.T> CASE e OF CSort ⇒x8 | CHead t⇒t
CHead (CSort O) (Bind Abst) (TSort O)
end of H25
suppose H26: eq C x7 (CSort O)
(H27)
consider H25
we proved
eq
T
<λ:C.T> CASE CHead x7 (Bind Abst) x8 OF CSort ⇒x8 | CHead t⇒t
<λ:C.T>
CASE CHead (CSort O) (Bind Abst) (TSort O) OF
CSort ⇒x8
| CHead t⇒t
that is equivalent to eq T x8 (TSort O)
we proceed by induction on the previous result to prove ty3 g x7 (TSort O) x9
case refl_equal : ⇒
the thesis becomes the hypothesis H13
ty3 g x7 (TSort O) x9
end of H27
by (ty3_gen_lref . . . . H22)
we proved
or
ex3_3
C
T
T
λ:C
.λ:T
.λt:T
.pc3
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
lift (S O) O t
x4
λe:C
.λu:T
.λ:T
.getl
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
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
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
lift (S O) O u
x4
λe:C
.λu:T
.λ:T
.getl
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
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 P
case or_introl : H30:ex3_3 C T T λ:C.λ:T.λt:T.pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O t) x4 λe:C.λu0:T.λ:T.getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H30 to prove P
case ex3_3_intro : x10:C x11:T x12:T :pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x12) x4 H32:getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x10 (Bind Abbr) x11) :ty3 g x10 x11 x12 ⇒
the thesis becomes P
(H34)
by (getl_gen_O . . H32)
we proved
clear
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x10 (Bind Abbr) x11
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x10 (Bind Abbr) x11
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O 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 x10 (Bind Abbr) x11 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 x10 (Bind Abbr) x11 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
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O 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 H34
consider H34
we proved
<λ:C.Prop>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O 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 P
P
P
case or_intror : H30:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4 λe:C.λu0:T.λ:T.getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0) λe:C.λu0:T.λt:T.ty3 g e u0 t ⇒
the thesis becomes P
we proceed by induction on H30 to prove P
case ex3_3_intro : x10:C x11:T x12:T H31:pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x11) x4 H32:getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x10 (Bind Abst) x11) H33:ty3 g x10 x11 x12 ⇒
the thesis becomes P
(H34)
by (getl_gen_O . . H32)
we proved
clear
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x10 (Bind Abst) x11
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x10 (Bind Abst) x11
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x10 (Bind Abst) x11 OF CSort ⇒x10 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O OF
CSort ⇒x10
| CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x10 | CHead c ⇒c (CHead x10 (Bind Abst) x11)
λe:C.<λ:C.C> CASE e OF CSort ⇒x10 | CHead c ⇒c
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
end of H34
(h1)
(H35)
by (getl_gen_O . . H32)
we proved
clear
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead x10 (Bind Abst) x11
by (clear_gen_bind . . . . previous)
we proved
eq
C
CHead x10 (Bind Abst) x11
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead x10 (Bind Abst) x11 OF CSort ⇒x11 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O OF
CSort ⇒x11
| CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒x11 | CHead t⇒t (CHead x10 (Bind Abst) x11)
λe:C.<λ:C.T> CASE e OF CSort ⇒x11 | CHead t⇒t
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
end of H35
suppose H36: eq C x10 (CHead (CSort O) (Bind Abst) (TSort O))
(H37)
consider H35
we proved
eq
T
<λ:C.T> CASE CHead x10 (Bind Abst) x11 OF CSort ⇒x11 | CHead t⇒t
<λ:C.T>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O OF
CSort ⇒x11
| CHead t⇒t
that is equivalent to eq T x11 (TSort O)
we proceed by induction on the previous result to prove ty3 g x10 (TSort O) x12
case refl_equal : ⇒
the thesis becomes the hypothesis H33
ty3 g x10 (TSort O) x12
end of H37
by (pc3_gen_abst . . . . . H7)
we proved
land
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
x0
∀b:B
.∀u:T
.pc3
CHead
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
Bind b
u
x5
x1
we proceed by induction on the previous result to prove P
case conj : H40:pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x0 :∀b:B.∀u0:T.(pc3 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind b) u0) x5 x1) ⇒
the thesis becomes P
(H42)
by (le_n .)
we proved le O O
by (lift_lref_ge . . . previous)
we proved eq T (lift (S O) O (TLRef O)) (TLRef (plus O (S O)))
we proceed by induction on the previous result to prove
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
TLRef (plus O (S O))
case refl_equal : ⇒
the thesis becomes
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
lift (S O) O (TLRef O)
consider H21
we proved
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O (TLRef O)
x0
that is equivalent to
ex2
T
λx:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O (TLRef O)
x
λx:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
x0
x
by (ex2_sym . . . previous)
we proved
ex2
T
λx:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
x0
x
λx:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
lift (S O) O (TLRef O)
x
that is equivalent to
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
x0
lift (S O) O (TLRef O)
by (pc3_t . . . H40 . previous)
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
lift (S O) O (TLRef O)
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
TLRef (plus O (S O))
end of H42
(H43) consider H42
consider H43
we proved
pc3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
TLRef (plus O (S O))
that is equivalent to
ex2
T
λt:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
t
λt:T
.pr3
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S O)
t
we proceed by induction on the previous result to prove P
case ex_intro2 : x13:T H44:pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x13 H45:pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x13 ⇒
the thesis becomes P
(H46)
(h1)
(h1)
by (clear_bind . . .)
clear
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
end of h1
(h2)
by (getl_refl . . .)
we proved
getl
O
CHead (CSort O) (Bind Abst) (TSort O)
CHead (CSort O) (Bind Abst) (TSort O)
that is equivalent to
getl
r (Bind Abst) O
CHead (CSort O) (Bind Abst) (TSort O)
CHead (CSort O) (Bind Abst) (TSort O)
by (getl_head . . . . previous .)
getl
S O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead (CSort O) (Bind Abst) (TSort O)
end of h2
by (getl_clear_bind . . . . h1 . . h2)
we proved
getl
S (S O)
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead (CSort O) (Bind Abst) (TSort O)
by (nf2_lref_abst . . . . previous)
we proved
nf2
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S (S O))
by (nf2_pr3_unfold . . . H44 previous)
eq T (TLRef (S (S O))) x13
end of h1
(h2)
by (getl_refl . . .)
we proved
getl
O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
that is equivalent to
getl
r (Bind Abst) O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
by (getl_head . . . . previous .)
we proved
getl
S O
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
by (nf2_lref_abst . . . . previous)
we proved
nf2
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
TLRef (S O)
by (nf2_pr3_unfold . . . H45 previous)
eq T (TLRef (S O)) x13
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (S (S O))) (TLRef (S O))
end of H46
(H47)
we proceed by induction on H46 to prove
<λ:T.Prop>
CASE TLRef (S O) OF
TSort ⇒False
| TLRef n⇒<λ:nat.Prop> CASE n OF O⇒False | S n0⇒<λ:nat.Prop> CASE n0 OF O⇒False | S ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef (S (S O)) OF
TSort ⇒False
| TLRef n⇒<λ:nat.Prop> CASE n OF O⇒False | S n0⇒<λ:nat.Prop> CASE n0 OF O⇒False | S ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef (S (S O)) OF
TSort ⇒False
| TLRef n⇒<λ:nat.Prop> CASE n OF O⇒False | S n0⇒<λ:nat.Prop> CASE n0 OF O⇒False | S ⇒True
| THead ⇒False
<λ:T.Prop>
CASE TLRef (S O) OF
TSort ⇒False
| TLRef n⇒<λ:nat.Prop> CASE n OF O⇒False | S n0⇒<λ:nat.Prop> CASE n0 OF O⇒False | S ⇒True
| THead ⇒False
end of H47
consider H47
we proved
<λ:T.Prop>
CASE TLRef (S O) OF
TSort ⇒False
| TLRef n⇒<λ:nat.Prop> CASE n OF O⇒False | S n0⇒<λ:nat.Prop> CASE n0 OF O⇒False | S ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
P
P
we proved P
(eq C x10 (CHead (CSort O) (Bind Abst) (TSort O)))→P
end of h1
(h2)
consider H34
we proved
eq
C
<λ:C.C> CASE CHead x10 (Bind Abst) x11 OF CSort ⇒x10 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O OF
CSort ⇒x10
| CHead c ⇒c
eq C x10 (CHead (CSort O) (Bind Abst) (TSort O))
end of h2
by (h1 h2)
P
P
we proved P
(eq C x7 (CSort O))→P
end of h1
(h2)
consider H24
we proved
eq
C
<λ:C.C> CASE CHead x7 (Bind Abst) x8 OF CSort ⇒x7 | CHead c ⇒c
<λ:C.C>
CASE CHead (CSort O) (Bind Abst) (TSort O) OF
CSort ⇒x7
| CHead c ⇒c
eq C x7 (CSort O)
end of h2
by (h1 h2)
we proved P
(eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O)
→P
end of h1
(h2)
consider H17
we proved
eq
C
<λ:C.C> CASE CHead x2 (Bind Abst) x3 OF CSort ⇒x2 | CHead c ⇒c
<λ:C.C>
CASE CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O OF
CSort ⇒x2
| CHead c ⇒c
eq
C
x2
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
end of h2
by (h1 h2)
P
P
P
P
P
P
P
we proved P
we proved
(ty3
g
CHead
CHead
CHead (CSort O) (Bind Abst) (TSort O)
Bind Abst
TSort O
Bind Abst
TLRef O
THead
Flat Appl
TLRef O
THead (Bind Abst) (TLRef (S (S O))) (TSort O)
u)
→∀P:Prop.P
that is equivalent to (ty3 g ex1_c ex1_t u)→∀P:Prop.P
we proved ∀g:G.∀u:T.(ty3 g ex1_c ex1_t u)→∀P:Prop.P