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