DEFINITION drop_gen_sort()
TYPE =
∀n:nat
.∀h:nat
.∀d:nat
.∀x:C
.drop h d (CSort n) x
→and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)
BODY =
assume n: nat
assume h: nat
assume d: nat
assume x: C
suppose H: drop h d (CSort n) x
assume y: C
suppose H0: drop h d y x
we proceed by induction on H0 to prove (eq C y (CSort n))→(and3 (eq C x y) (eq nat h O) (eq nat d O))
case drop_refl : c:C ⇒
the thesis becomes ∀H1:(eq C c (CSort n)).(and3 (eq C c c) (eq nat O O) (eq nat O O))
suppose H1: eq C c (CSort n)
(H2)
by (f_equal . . . . . H1)
we proved eq C c (CSort n)
eq C (λe:C.e c) (λe:C.e (CSort n))
end of H2
(h1)
by (refl_equal . .)
eq C (CSort n) (CSort n)
end of h1
(h2)
by (refl_equal . .)
eq nat O O
end of h2
(h3)
by (refl_equal . .)
eq nat O O
end of h3
by (and3_intro . . . h1 h2 h3)
we proved and3 (eq C (CSort n) (CSort n)) (eq nat O O) (eq nat O O)
by (eq_ind_r . . . previous . H2)
we proved and3 (eq C c c) (eq nat O O) (eq nat O O)
∀H1:(eq C c (CSort n)).(and3 (eq C c c) (eq nat O O) (eq nat O O))
case drop_drop : k:K h0:nat c:C e:C :drop (r k h0) O c e u:T ⇒
the thesis becomes
∀H3:eq C (CHead c k u) (CSort n)
.and3 (eq C e (CHead c k u)) (eq nat (S h0) O) (eq nat O O)
() by induction hypothesis we know
eq C c (CSort n)
→and3 (eq C e c) (eq nat (r k h0) O) (eq nat O O)
suppose H3: eq C (CHead c k u) (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 c k u OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c k u 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 and3 (eq C e (CHead c k u)) (eq nat (S h0) O) (eq nat O O)
we proved and3 (eq C e (CHead c k u)) (eq nat (S h0) O) (eq nat O O)
∀H3:eq C (CHead c k u) (CSort n)
.and3 (eq C e (CHead c k u)) (eq nat (S h0) O) (eq nat O O)
case drop_skip : k:K h0:nat d0:nat c:C e:C :drop h0 (r k d0) c e u:T ⇒
the thesis becomes
∀H3:eq C (CHead c k (lift h0 (r k d0) u)) (CSort n)
.and3
eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))
eq nat h0 O
eq nat (S d0) O
() by induction hypothesis we know
(eq C c (CSort n))→(and3 (eq C e c) (eq nat h0 O) (eq nat (r k d0) O))
suppose H3: eq C (CHead c k (lift h0 (r k d0) u)) (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 c k (lift h0 (r k d0) u) OF
CSort ⇒False
| CHead ⇒True
consider I
we proved True
<λ:C.Prop>
CASE CHead c k (lift h0 (r k d0) u) 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
and3
eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))
eq nat h0 O
eq nat (S d0) O
we proved
and3
eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))
eq nat h0 O
eq nat (S d0) O
∀H3:eq C (CHead c k (lift h0 (r k d0) u)) (CSort n)
.and3
eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))
eq nat h0 O
eq nat (S d0) O
we proved (eq C y (CSort n))→(and3 (eq C x y) (eq nat h O) (eq nat d O))
we proved
∀y:C
.drop h d y x
→(eq C y (CSort n))→(and3 (eq C x y) (eq nat h O) (eq nat d O))
by (insert_eq . . . . previous H)
we proved and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)
we proved
∀n:nat
.∀h:nat
.∀d:nat
.∀x:C
.drop h d (CSort n) x
→and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)