DEFINITION drop_clear_S()
TYPE =
∀x2:C
.∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 x2
→∀b:B
.∀c2:C
.∀u:T
.clear x2 (CHead c2 (Bind b) u)
→ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
BODY =
assume x2: C
we proceed by induction on x2 to prove
∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 x2
→∀b:B
.∀c2:C
.∀u:T
.clear x2 (CHead c2 (Bind b) u)
→ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
case CSort : n:nat ⇒
the thesis becomes
∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 (CSort n)
→∀b:B
.∀c2:C
.∀u:T
.∀H0:clear (CSort n) (CHead c2 (Bind b) u)
.ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
assume x1: C
assume h: nat
assume d: nat
suppose : drop h (S d) x1 (CSort n)
assume b: B
assume c2: C
assume u: T
suppose H0: clear (CSort n) (CHead c2 (Bind b) u)
by (clear_gen_sort . . H0 .)
we proved ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 (CSort n)
→∀b:B
.∀c2:C
.∀u:T
.∀H0:clear (CSort n) (CHead c2 (Bind b) u)
.ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀x1:C
.∀h:nat
.∀d:nat
.∀H0:drop h (S d) x1 (CHead c k t)
.∀b:B
.∀c2:C
.∀u:T
.∀H1:clear (CHead c k t) (CHead c2 (Bind b) u)
.ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
(H) by induction hypothesis we know
∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 c
→∀b:B
.∀c2:C
.∀u:T
.clear c (CHead c2 (Bind b) u)
→ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
assume x1: C
assume h: nat
assume d: nat
suppose H0: drop h (S d) x1 (CHead c k t)
assume b: B
assume c2: C
assume u: T
suppose H1: clear (CHead c k t) (CHead c2 (Bind b) u)
by (drop_gen_skip_r . . . . . . H0)
we proved
ex2 C λe:C.eq C x1 (CHead e k (lift h (r k d) t)) λe:C.drop h (r k d) e c
we proceed by induction on the previous result to prove ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
case ex_intro2 : x:C H2:eq C x1 (CHead x k (lift h (r k d) t)) H3:drop h (r k d) x c ⇒
the thesis becomes ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
assume b0: B
suppose H4: clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u)
suppose H5: drop h (r (Bind b0) d) x c
(H6)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead c2 (Bind b) u) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind b) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c (Bind b0) t)
end of H6
(h1)
(H7)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead c2 (Bind b) u) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c (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 c2 (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 c (Bind b0) t
end of H7
(h1)
(H8)
by (clear_gen_bind . . . . H4)
we proved eq C (CHead c2 (Bind b) u) (CHead c (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b0) t OF CSort ⇒u | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c2 (Bind b) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t0⇒t0 (CHead c (Bind b0) t)
end of H8
suppose H9: eq B b b0
suppose H10: eq C c2 c
(h1)
(h1)
by (clear_bind . . .)
we proved
clear
CHead x (Bind b0) (lift h d t)
CHead x (Bind b0) (lift h d t)
clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead x (Bind b0) (lift h d t)
end of h1
(h2)
consider H5
we proved drop h (r (Bind b0) d) x c
drop h d x c
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b0) (lift h d t)
λc1:C.drop h d c1 c
by (eq_ind_r . . . previous . H9)
we proved
ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d t)
λc1:C.drop h d c1 c
by (eq_ind_r . . . previous . H10)
ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d t)
λc1:C.drop h d c1 c2
end of h1
(h2)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b0) t OF CSort ⇒u | CHead t0⇒t0
eq T u t
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
eq B b b0
→(eq C c2 c
→(ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2))
end of h1
(h2)
consider H7
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c (Bind b0) t OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of h2
by (h1 h2)
eq C c2 c
→(ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead c (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 c
end of h2
by (h1 h2)
we proved
ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
∀H4:clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u)
.∀H5:drop h (r (Bind b0) d) x c
.ex2
C
λc1:C
.clear
CHead x (Bind b0) (lift h (r (Bind b0) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
assume f: F
suppose H4: clear (CHead c (Flat f) t) (CHead c2 (Bind b) u)
suppose H5: drop h (r (Flat f) d) x c
(H6)
(h1)
consider H5
we proved drop h (r (Flat f) d) x c
drop h (S d) x c
end of h1
(h2)
by (clear_gen_flat . . . . H4)
clear c (CHead c2 (Bind b) u)
end of h2
by (H . . . h1 . . . h2)
ex2 C λc1:C.clear x (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
end of H6
we proceed by induction on H6 to prove
ex2
C
λc1:C
.clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
case ex_intro2 : x0:C H7:clear x (CHead x0 (Bind b) (lift h d u)) H8:drop h d x0 c2 ⇒
the thesis becomes
ex2
C
λc1:C
.clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
by (clear_flat . . H7 . .)
we proved
clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead x0 (Bind b) (lift h d u)
by (ex_intro2 . . . . previous H8)
ex2
C
λc1:C
.clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
we proved
ex2
C
λc1:C
.clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
∀H4:clear (CHead c (Flat f) t) (CHead c2 (Bind b) u)
.∀H5:drop h (r (Flat f) d) x c
.ex2
C
λc1:C
.clear
CHead x (Flat f) (lift h (r (Flat f) d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
by (previous . H1 H3)
we proved
ex2
C
λc1:C
.clear
CHead x k (lift h (r k d) t)
CHead c1 (Bind b) (lift h d u)
λc1:C.drop h d c1 c2
by (eq_ind_r . . . previous . H2)
ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
we proved ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
∀x1:C
.∀h:nat
.∀d:nat
.∀H0:drop h (S d) x1 (CHead c k t)
.∀b:B
.∀c2:C
.∀u:T
.∀H1:clear (CHead c k t) (CHead c2 (Bind b) u)
.ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
we proved
∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 x2
→∀b:B
.∀c2:C
.∀u:T
.clear x2 (CHead c2 (Bind b) u)
→ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
we proved
∀x2:C
.∀x1:C
.∀h:nat
.∀d:nat
.drop h (S d) x1 x2
→∀b:B
.∀c2:C
.∀u:T
.clear x2 (CHead c2 (Bind b) u)
→ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2