DEFINITION getl_drop()
TYPE =
∀b:B
.∀c:C
.∀e:C.∀u:T.∀h:nat.(getl h 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.(getl h 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:getl h (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: getl h (CSort n) (CHead e (Bind b) u)
by (getl_gen_sort . . . H .)
we proved drop (S h) O (CSort n) e
∀e:C
.∀u:T
.∀h:nat
.∀H:getl h (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
.getl h (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.(getl h 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
getl h (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
case O : ⇒
the thesis becomes
getl O (CHead c0 k t) (CHead e (Bind b) u)
→drop (S O) O (CHead c0 k t) e
suppose H0: getl O (CHead c0 k t) (CHead e (Bind b) u)
by (getl_gen_O . . H0)
we proved clear (CHead c0 k t) (CHead e (Bind b) u)
assume b0: B
suppose H1: clear (CHead c0 (Bind b0) t) (CHead e (Bind b) u)
(H2)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead e (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead e (Bind b) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead c0 (Bind b0) t)
end of H2
(h1)
(H3)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead e (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c0 (Bind b0) t OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead e (Bind b) u
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead c0 (Bind b0) t
end of H3
(H5)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c0 (Bind b0) t OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of H5
suppose H6: eq C e c0
we proceed by induction on H5 to prove drop (S O) O (CHead c0 (Bind b0) t) c0
case refl_equal : ⇒
the thesis becomes drop (S O) O (CHead c0 (Bind b) 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 .)
drop (S O) O (CHead c0 (Bind b) t) c0
we proved drop (S O) O (CHead c0 (Bind b0) t) c0
by (eq_ind_r . . . previous . H6)
we proved drop (S O) O (CHead c0 (Bind b0) t) e
(eq C e c0)→(drop (S O) O (CHead c0 (Bind b0) t) e)
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e | CHead c1 ⇒c1
eq C e c0
end of h2
by (h1 h2)
we proved drop (S O) O (CHead c0 (Bind b0) t) e
∀H1:clear (CHead c0 (Bind b0) t) (CHead e (Bind b) u)
.drop (S O) O (CHead c0 (Bind b0) t) e
assume f: F
suppose H1: clear (CHead c0 (Flat f) t) (CHead e (Bind b) u)
(h1)
by (clear_gen_flat . . . . H1)
we proved clear c0 (CHead e (Bind b) u)
by (clear_flat . . previous . .)
clear (CHead c0 (Flat f) t) (CHead e (Bind b) u)
end of h1
(h2)
by (drop_refl .)
drop O O e e
end of h2
by (drop_clear_O . . . . h1 . . h2)
we proved drop (S O) O (CHead c0 (Flat f) t) e
∀H1:clear (CHead c0 (Flat f) t) (CHead e (Bind b) u)
.drop (S O) O (CHead c0 (Flat f) t) e
by (previous . previous)
we proved drop (S O) O (CHead c0 k t) e
getl 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:getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
.drop (S (S n)) O (CHead c0 k t) e
() by induction hypothesis we know
getl n (CHead c0 k t) (CHead e (Bind b) u)
→drop (S n) O (CHead c0 k t) e
suppose H1: getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
(h1)
by (getl_gen_S . . . . . H1)
we proved getl (r k n) 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:getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
.drop (S (S n)) O (CHead c0 k t) e
we proved
getl h (CHead c0 k t) (CHead e (Bind b) u)
→drop (S h) O (CHead c0 k t) e
∀e:C
.∀u:T
.∀h:nat
.getl h (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.(getl h c (CHead e (Bind b) u))→(drop (S h) O c e)
we proved
∀b:B
.∀c:C
.∀e:C.∀u:T.∀h:nat.(getl h c (CHead e (Bind b) u))→(drop (S h) O c e)