DEFINITION drop_S()
TYPE =
∀b:B
.∀c:C
.∀e:C
.∀u:T.∀h:nat.(drop h O c (CHead e (Bind b) u))→(drop (S h) O c e)
BODY =
assume b: B
assume c: C
we proceed by induction on c to prove
∀e:C
.∀u:T.∀h:nat.(drop h O c (CHead e (Bind b) u))→(drop (S h) O c e)
case CSort : n:nat ⇒
the thesis becomes
∀e:C
.∀u:T
.∀h:nat
.∀H:drop h O (CSort n) (CHead e (Bind b) u)
.drop (S h) O (CSort n) e
assume e: C
assume u: T
assume h: nat
suppose H: drop h O (CSort n) (CHead e (Bind b) u)
by (drop_gen_sort . . . . H)
we proved
and3
eq C (CHead e (Bind b) u) (CSort n)
eq nat h O
eq nat O O
we proceed by induction on the previous result to prove drop (S h) O (CSort n) e
case and3_intro : H0:eq C (CHead e (Bind b) u) (CSort n) H1:eq nat h O :eq nat O O ⇒
the thesis becomes drop (S h) O (CSort n) e
(H3)
we proceed by induction on H0 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop> CASE CHead e (Bind b) u OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead e (Bind b) u OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H3
consider H3
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 drop (S O) O (CSort n) e
we proved drop (S O) O (CSort n) e
by (eq_ind_r . . . previous . H1)
drop (S h) O (CSort n) e
we proved drop (S h) O (CSort n) e
∀e:C
.∀u:T
.∀h:nat
.∀H:drop h O (CSort n) (CHead e (Bind b) u)
.drop (S h) O (CSort n) e
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀e:C
.∀u:T
.∀h:nat
.drop h O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
(H) by induction hypothesis we know ∀e:C.∀u:T.∀h:nat.(drop h O c0 (CHead e (Bind b) u))→(drop (S h) O c0 e)
assume e: C
assume u: T
assume h: nat
we proceed by induction on h to prove
drop h O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
case O : ⇒
the thesis becomes
drop O O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S O) O (CHead c0 k t) e
suppose H0: drop O O (CHead c0 k t) (CHead e (Bind b) u)
(H1)
by (drop_gen_refl . . H0)
we proved eq C (CHead c0 k t) (CHead e (Bind b) u)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c0 k t OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒c0 | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c0 k t)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead e (Bind b) u)
end of H1
(h1)
(H2)
by (drop_gen_refl . . H0)
we proved eq C (CHead c0 k t) (CHead e (Bind b) u)
by (f_equal . . . . . previous)
we proved
eq
K
<λ:C.K> CASE CHead c0 k t OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead e (Bind b) u OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k | CHead k0 ⇒k0 (CHead c0 k t)
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k | CHead k0 ⇒k0 (CHead e (Bind b) u)
end of H2
(H4)
consider H2
we proved
eq
K
<λ:C.K> CASE CHead c0 k t OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead e (Bind b) u OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind b)
end of H4
suppose H5: eq C c0 e
we proceed by induction on H5 to prove drop (S O) O (CHead c0 k t) e
case refl_equal : ⇒
the thesis becomes drop (S O) O (CHead c0 k t) c0
by (drop_refl .)
we proved drop O O c0 c0
that is equivalent to drop (r (Bind b) O) O c0 c0
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c0 (Bind b) t) c0
by (eq_ind_r . . . previous . H4)
drop (S O) O (CHead c0 k t) c0
we proved drop (S O) O (CHead c0 k t) e
(eq C c0 e)→(drop (S O) O (CHead c0 k t) e)
end of h1
(h2)
consider H1
we proved
eq
C
<λ:C.C> CASE CHead c0 k t OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒c0 | CHead c1 ⇒c1
eq C c0 e
end of h2
by (h1 h2)
we proved drop (S O) O (CHead c0 k t) e
drop O O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S O) O (CHead c0 k t) e
case S : n:nat ⇒
the thesis becomes
∀H1:drop (S n) O (CHead c0 k t) (CHead e (Bind b) u)
.drop (S (S n)) O (CHead c0 k t) e
() by induction hypothesis we know
drop n O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S n) O (CHead c0 k t) e
suppose H1: drop (S n) O (CHead c0 k t) (CHead e (Bind b) u)
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r k n) O c0 (CHead e (Bind b) u)
by (H . . . previous)
drop (S (r k n)) O c0 e
end of h1
(h2)
by (r_S . .)
eq nat (r k (S n)) (S (r k n))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved drop (r k (S n)) O c0 e
by (drop_drop . . . . previous .)
we proved drop (S (S n)) O (CHead c0 k t) e
∀H1:drop (S n) O (CHead c0 k t) (CHead e (Bind b) u)
.drop (S (S n)) O (CHead c0 k t) e
we proved
drop h O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
∀e:C
.∀u:T
.∀h:nat
.drop h O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
we proved
∀e:C
.∀u:T.∀h:nat.(drop h O c (CHead e (Bind b) u))→(drop (S h) O c e)
we proved
∀b:B
.∀c:C
.∀e:C
.∀u:T.∀h:nat.(drop h O c (CHead e (Bind b) u))→(drop (S h) O c e)