DEFINITION csubc_gen_sort_r()
TYPE =
∀g:G.∀x:C.∀n:nat.(csubc g x (CSort n))→(eq C x (CSort n))
BODY =
assume g: G
assume x: C
assume n: nat
suppose H: csubc g x (CSort n)
assume y: C
suppose H0: csubc g x y
we proceed by induction on H0 to prove (eq C y (CSort n))→(eq C x y)
case csubc_sort : n0:nat ⇒
the thesis becomes ∀H1:(eq C (CSort n0) (CSort n)).(eq C (CSort n0) (CSort n0))
suppose H1: eq C (CSort n0) (CSort n)
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:C.nat> CASE CSort n0 OF CSort n1⇒n1 | CHead ⇒n0
<λ:C.nat> CASE CSort n OF CSort n1⇒n1 | CHead ⇒n0
eq
nat
λe:C.<λ:C.nat> CASE e OF CSort n1⇒n1 | CHead ⇒n0 (CSort n0)
λe:C.<λ:C.nat> CASE e OF CSort n1⇒n1 | CHead ⇒n0 (CSort n)
end of H2
(h1)
by (refl_equal . .)
eq C (CSort n) (CSort n)
end of h1
(h2)
consider H2
we proved
eq
nat
<λ:C.nat> CASE CSort n0 OF CSort n1⇒n1 | CHead ⇒n0
<λ:C.nat> CASE CSort n OF CSort n1⇒n1 | CHead ⇒n0
eq nat n0 n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq C (CSort n0) (CSort n0)
∀H1:(eq C (CSort n0) (CSort n)).(eq C (CSort n0) (CSort n0))
case csubc_head : c1:C c2:C :csubc g c1 c2 k:K v:T ⇒
the thesis becomes ∀H3:(eq C (CHead c2 k v) (CSort n)).(eq C (CHead c1 k v) (CHead c2 k v))
() by induction hypothesis we know (eq C c2 (CSort n))→(eq C c1 c2)
suppose H3: eq C (CHead c2 k v) (CSort n)
(H4)
we proceed by induction on H3 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CHead c2 k v OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c2 k v OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H4
consider H4
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq C (CHead c1 k v) (CHead c2 k v)
we proved eq C (CHead c1 k v) (CHead c2 k v)
∀H3:(eq C (CHead c2 k v) (CSort n)).(eq C (CHead c1 k v) (CHead c2 k v))
case csubc_void : c1:C c2:C :csubc g c1 c2 b:B :not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀H4:eq C (CHead c2 (Bind b) u2) (CSort n)
.eq C (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2)
() by induction hypothesis we know (eq C c2 (CSort n))→(eq C c1 c2)
suppose H4: eq C (CHead c2 (Bind b) u2) (CSort n)
(H5)
we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CHead c2 (Bind b) u2 OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c2 (Bind b) u2 OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H5
consider H5
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq C (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2)
we proved eq C (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2)
∀H4:eq C (CHead c2 (Bind b) u2) (CSort n)
.eq C (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2)
case csubc_abst : c1:C c2:C :csubc g c1 c2 v:T a:A :sc3 g (asucc g a) c1 v w:T :sc3 g a c2 w ⇒
the thesis becomes
∀H5:eq C (CHead c2 (Bind Abbr) w) (CSort n)
.eq C (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)
() by induction hypothesis we know (eq C c2 (CSort n))→(eq C c1 c2)
suppose H5: eq C (CHead c2 (Bind Abbr) w) (CSort n)
(H6)
we proceed by induction on H5 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead c2 (Bind Abbr) w OF
CSort ⇒False
| CHead ⇒True
consider I
we proved True
<λ:C.Prop>
CASE CHead c2 (Bind Abbr) w OF
CSort ⇒False
| CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H6
consider H6
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq C (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)
we proved eq C (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)
∀H5:eq C (CHead c2 (Bind Abbr) w) (CSort n)
.eq C (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)
we proved (eq C y (CSort n))→(eq C x y)
we proved ∀y:C.(csubc g x y)→(eq C y (CSort n))→(eq C x y)
by (insert_eq . . . . previous H)
we proved eq C x (CSort n)
we proved ∀g:G.∀x:C.∀n:nat.(csubc g x (CSort n))→(eq C x (CSort n))