DEFINITION drop_clear_O()
TYPE =
∀b:B
.∀c:C
.∀e1:C
.∀u:T
.clear c (CHead e1 (Bind b) u)
→∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c e2)
BODY =
assume b: B
assume c: C
we proceed by induction on c to prove
∀e1:C
.∀u:T
.clear c (CHead e1 (Bind b) u)
→∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c e2)
case CSort : n:nat ⇒
the thesis becomes
∀e1:C
.∀u:T
.∀H:clear (CSort n) (CHead e1 (Bind b) u)
.∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O (CSort n) e2)
assume e1: C
assume u: T
suppose H: clear (CSort n) (CHead e1 (Bind b) u)
assume e2: C
assume i: nat
suppose : drop i O e1 e2
by (clear_gen_sort . . H .)
we proved drop (S i) O (CSort n) e2
∀e1:C
.∀u:T
.∀H:clear (CSort n) (CHead e1 (Bind b) u)
.∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O (CSort n) e2)
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀e1:C
.∀u:T
.∀H0:clear (CHead c0 k t) (CHead e1 (Bind b) u)
.∀e2:C.∀i:nat.∀H1:(drop i O e1 e2).(drop (S i) O (CHead c0 k t) e2)
(H) by induction hypothesis we know
∀e1:C
.∀u:T
.clear c0 (CHead e1 (Bind b) u)
→∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c0 e2)
assume e1: C
assume u: T
suppose H0: clear (CHead c0 k t) (CHead e1 (Bind b) u)
assume e2: C
assume i: nat
suppose H1: drop i O e1 e2
assume b0: B
suppose H2: clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) u)
(H3)
by (clear_gen_bind . . . . H2)
we proved eq C (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e1 (Bind b) u OF CSort ⇒e1 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e1 | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c1 ⇒c1 (CHead e1 (Bind b) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c1 ⇒c1 (CHead c0 (Bind b0) t)
end of H3
(h1)
(H4)
by (clear_gen_bind . . . . H2)
we proved eq C (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead e1 (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
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead e1 (Bind b) u
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead c0 (Bind b0) t
end of H4
(H6)
consider H4
we proved
eq
B
<λ:C.B>
CASE CHead e1 (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 H6
suppose H7: eq C e1 c0
(H8)
we proceed by induction on H7 to prove drop i O c0 e2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
drop i O c0 e2
end of H8
we proceed by induction on H6 to prove drop (S i) O (CHead c0 (Bind b0) t) e2
case refl_equal : ⇒
the thesis becomes drop (S i) O (CHead c0 (Bind b) t) e2
consider H8
we proved drop i O c0 e2
that is equivalent to drop (r (Bind b) i) O c0 e2
by (drop_drop . . . . previous .)
drop (S i) O (CHead c0 (Bind b) t) e2
we proved drop (S i) O (CHead c0 (Bind b0) t) e2
(eq C e1 c0)→(drop (S i) O (CHead c0 (Bind b0) t) e2)
end of h1
(h2)
consider H3
we proved
eq
C
<λ:C.C> CASE CHead e1 (Bind b) u OF CSort ⇒e1 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e1 | CHead c1 ⇒c1
eq C e1 c0
end of h2
by (h1 h2)
we proved drop (S i) O (CHead c0 (Bind b0) t) e2
∀H2:clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) u)
.drop (S i) O (CHead c0 (Bind b0) t) e2
assume f: F
suppose H2: clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) u)
by (clear_gen_flat . . . . H2)
we proved clear c0 (CHead e1 (Bind b) u)
by (H . . previous . . H1)
we proved drop (S i) O c0 e2
that is equivalent to drop (r (Flat f) i) O c0 e2
by (drop_drop . . . . previous .)
we proved drop (S i) O (CHead c0 (Flat f) t) e2
∀H2:clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) u)
.drop (S i) O (CHead c0 (Flat f) t) e2
by (previous . H0)
we proved drop (S i) O (CHead c0 k t) e2
∀e1:C
.∀u:T
.∀H0:clear (CHead c0 k t) (CHead e1 (Bind b) u)
.∀e2:C.∀i:nat.∀H1:(drop i O e1 e2).(drop (S i) O (CHead c0 k t) e2)
we proved
∀e1:C
.∀u:T
.clear c (CHead e1 (Bind b) u)
→∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c e2)
we proved
∀b:B
.∀c:C
.∀e1:C
.∀u:T
.clear c (CHead e1 (Bind b) u)
→∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c e2)