DEFINITION getl_drop_conf_lt()
TYPE =
∀b:B
.∀c:C
.∀c0:C
.∀u:T
.∀i:nat
.getl i c (CHead c0 (Bind b) u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c0 e0)
BODY =
assume b: B
assume c: C
we proceed by induction on c to prove
∀c1:C
.∀u:T
.∀i:nat
.getl i c (CHead c1 (Bind b) u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)
case CSort : n:nat ⇒
the thesis becomes
∀c0:C
.∀u:T
.∀i:nat
.∀H:getl i (CSort n) (CHead c0 (Bind b) u)
.∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) (CSort n) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c0 e0)
assume c0: C
assume u: T
assume i: nat
suppose H: getl i (CSort n) (CHead c0 (Bind b) u)
assume e: C
assume h: nat
assume d: nat
suppose : drop h (S (plus i d)) (CSort n) e
by (getl_gen_sort . . . H .)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c0 e0
∀c0:C
.∀u:T
.∀i:nat
.∀H:getl i (CSort n) (CHead c0 (Bind b) u)
.∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) (CSort n) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c0 e0)
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀c1:C
.∀u:T
.∀i:nat
.∀H0:getl i (CHead c0 k t) (CHead c1 (Bind b) u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h (S (plus i d)) (CHead c0 k t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(H) by induction hypothesis we know
∀c1:C
.∀u:T
.∀i:nat
.getl i c0 (CHead c1 (Bind b) u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) c0 e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)
assume c1: C
assume u: T
assume i: nat
suppose H0: getl i (CHead c0 k t) (CHead c1 (Bind b) u)
assume e: C
assume h: nat
assume d: nat
suppose H1: drop h (S (plus i d)) (CHead c0 k t) e
(H2)
by (getl_gen_all . . . H0)
ex2 C λe:C.drop i O (CHead c0 k t) e λe:C.clear e (CHead c1 (Bind b) u)
end of H2
we proceed by induction on H2 to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex_intro2 : x:C H3:drop i O (CHead c0 k t) x H4:clear x (CHead c1 (Bind b) u) ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
assume n: nat
suppose : drop i O (CHead c0 k t) (CSort n)
suppose H6: clear (CSort n) (CHead c1 (Bind b) u)
by (clear_gen_sort . . H6 .)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
drop i O (CHead c0 k t) (CSort n)
→∀H6:clear (CSort n) (CHead c1 (Bind b) u)
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
assume x0: C
suppose IHx:
drop i O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
assume k0: K
assume t0: T
suppose H5: drop i O (CHead c0 k t) (CHead x0 k0 t0)
suppose H6: clear (CHead x0 k0 t0) (CHead c1 (Bind b) u)
assume b0: B
suppose H7: drop i O (CHead c0 k t) (CHead x0 (Bind b0) t0)
suppose H8: clear (CHead x0 (Bind b0) t0) (CHead c1 (Bind b) u)
(H9)
by (clear_gen_bind . . . . H8)
we proved eq C (CHead c1 (Bind b) u) (CHead x0 (Bind b0) t0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c2 ⇒c2
<λ:C.C> CASE CHead x0 (Bind b0) t0 OF CSort ⇒c1 | CHead c2 ⇒c2
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c1 | CHead c2 ⇒c2 (CHead c1 (Bind b) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c1 | CHead c2 ⇒c2 (CHead x0 (Bind b0) t0)
end of H9
(h1)
(H10)
by (clear_gen_bind . . . . H8)
we proved eq C (CHead c1 (Bind b) u) (CHead x0 (Bind b0) t0)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead c1 (Bind b) u OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead x0 (Bind b0) t0 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead c1 (Bind b) u
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead x0 (Bind b0) t0
end of H10
(h1)
(H11)
by (clear_gen_bind . . . . H8)
we proved eq C (CHead c1 (Bind b) u) (CHead x0 (Bind b0) t0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind b) u OF CSort ⇒u | CHead t1⇒t1
<λ:C.T> CASE CHead x0 (Bind b0) t0 OF CSort ⇒u | CHead t1⇒t1
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t1⇒t1 (CHead c1 (Bind b) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t1⇒t1 (CHead x0 (Bind b0) t0)
end of H11
suppose H12: eq B b b0
suppose H13: eq C c1 x0
(H14)
consider H11
we proved
eq
T
<λ:C.T> CASE CHead c1 (Bind b) u OF CSort ⇒u | CHead t1⇒t1
<λ:C.T> CASE CHead x0 (Bind b0) t0 OF CSort ⇒u | CHead t1⇒t1
that is equivalent to eq T u t0
by (eq_ind_r . . . H7 . previous)
drop i O (CHead c0 k t) (CHead x0 (Bind b0) u)
end of H14
(H15)
by (eq_ind_r . . . H14 . H12)
drop i O (CHead c0 k t) (CHead x0 (Bind b) u)
end of H15
(H16)
by (eq_ind_r . . . IHx . H13)
drop i O (CHead c0 k t) c1
→(clear c1 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H16
(H17)
by (eq_ind_r . . . H15 . H13)
drop i O (CHead c0 k t) (CHead c1 (Bind b) u)
end of H17
by (drop_conf_lt . . . . . H17 . . . H1)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r (Bind b) d) v)
λv:T.λe0:C.drop i O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h (r (Bind b) d) c1 e0
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex3_2_intro : x1:T x2:C H18:eq T u (lift h (r (Bind b) d) x1) H19:drop i O e (CHead x2 (Bind b) x1) H20:drop h (r (Bind b) d) c1 x2 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(h1)
by (refl_equal . .)
we proved eq T (lift h d x1) (lift h d x1)
eq T (lift h (r (Bind b) d) x1) (lift h d x1)
end of h1
(h2)
by (clear_bind . . .)
we proved clear (CHead x2 (Bind b) x1) (CHead x2 (Bind b) x1)
by (getl_intro . . . . H19 previous)
getl i e (CHead x2 (Bind b) x1)
end of h2
(h3)
consider H20
we proved drop h (r (Bind b) d) c1 x2
drop h d c1 x2
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
C
λv:T.λ:C.eq T (lift h (r (Bind b) d) x1) (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (eq_ind_r . . . previous . H18)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
eq B b b0
→(eq C c1 x0
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of h1
(h2)
consider H10
we proved
eq
B
<λ:C.B>
CASE CHead c1 (Bind b) u OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead x0 (Bind b0) t0 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of h2
by (h1 h2)
eq C c1 x0
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead c1 (Bind b) u OF CSort ⇒c1 | CHead c2 ⇒c2
<λ:C.C> CASE CHead x0 (Bind b0) t0 OF CSort ⇒c1 | CHead c2 ⇒c2
eq C c1 x0
end of h2
by (h1 h2)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
∀H7:drop i O (CHead c0 k t) (CHead x0 (Bind b0) t0)
.∀H8:clear (CHead x0 (Bind b0) t0) (CHead c1 (Bind b) u)
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
assume f: F
suppose H7: drop i O (CHead c0 k t) (CHead x0 (Flat f) t0)
suppose H8: clear (CHead x0 (Flat f) t0) (CHead c1 (Bind b) u)
suppose H9: drop h (S (plus O d)) (CHead c0 k t) e
suppose H10: drop O O (CHead c0 k t) (CHead x0 (Flat f) t0)
suppose IHx0:
drop O O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
(H11)
by (drop_gen_refl . . H10)
we proved eq C (CHead c0 k t) (CHead x0 (Flat f) t0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c0 k t OF CSort ⇒c0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead x0 (Flat f) t0 OF CSort ⇒c0 | CHead c2 ⇒c2
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c2 ⇒c2 (CHead c0 k t)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c2 ⇒c2 (CHead x0 (Flat f) t0)
end of H11
(h1)
(H12)
by (drop_gen_refl . . H10)
we proved eq C (CHead c0 k t) (CHead x0 (Flat f) t0)
by (f_equal . . . . . previous)
we proved
eq
K
<λ:C.K> CASE CHead c0 k t OF CSort ⇒k | CHead k1 ⇒k1
<λ:C.K> CASE CHead x0 (Flat f) t0 OF CSort ⇒k | CHead k1 ⇒k1
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k | CHead k1 ⇒k1 (CHead c0 k t)
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k | CHead k1 ⇒k1 (CHead x0 (Flat f) t0)
end of H12
(H14)
consider H12
we proved
eq
K
<λ:C.K> CASE CHead c0 k t OF CSort ⇒k | CHead k1 ⇒k1
<λ:C.K> CASE CHead x0 (Flat f) t0 OF CSort ⇒k | CHead k1 ⇒k1
eq K k (Flat f)
end of H14
suppose H15: eq C c0 x0
(H16)
by (clear_gen_flat . . . . H8)
we proved clear x0 (CHead c1 (Bind b) u)
by (eq_ind_r . . . previous . H15)
clear c0 (CHead c1 (Bind b) u)
end of H16
(H17)
by (eq_ind_r . . . IHx0 . H15)
drop O O (CHead c0 k t) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H17
(H18)
we proceed by induction on H14 to prove
drop O O (CHead c0 (Flat f) t) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H17
drop O O (CHead c0 (Flat f) t) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H18
(H19)
we proceed by induction on H14 to prove drop h (S (plus O d)) (CHead c0 (Flat f) t) e
case refl_equal : ⇒
the thesis becomes the hypothesis H9
drop h (S (plus O d)) (CHead c0 (Flat f) t) e
end of H19
by (drop_gen_skip_l . . . . . . H19)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e (Flat f) v)
λ:C.λv:T.eq T t (lift h (r (Flat f) (plus O d)) v)
λe:C.λ:T.drop h (r (Flat f) (plus O d)) c0 e
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex3_2_intro : x1:C x2:T H20:eq C e (CHead x1 (Flat f) x2) H21:eq T t (lift h (r (Flat f) (plus O d)) x2) H22:drop h (r (Flat f) (plus O d)) c0 x1 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(H23)
by (f_equal . . . . . H21)
we proved eq T t (lift h (r (Flat f) (plus O d)) x2)
eq T (λe0:T.e0 t) (λe0:T.e0 (lift h (r (Flat f) (plus O d)) x2))
end of H23
(H24)
we proceed by induction on H20 to prove
drop O O (CHead c0 (Flat f) t) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H18
drop O O (CHead c0 (Flat f) t) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H24
(H25)
consider H23
we proved eq T t (lift h (r (Flat f) (plus O d)) x2)
that is equivalent to eq T t (lift h (S d) x2)
we proceed by induction on the previous result to prove
drop O O (CHead c0 (Flat f) (lift h (S d) x2)) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H24
drop O O (CHead c0 (Flat f) (lift h (S d) x2)) c0
→(clear c0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H25
(H26)
(h1)
by (drop_refl .)
we proved drop O O c0 c0
by (getl_intro . . . . previous H16)
getl O c0 (CHead c1 (Bind b) u)
end of h1
(h2)
consider H22
we proved drop h (r (Flat f) (plus O d)) c0 x1
drop h (S (plus O d)) c0 x1
end of h2
by (H . . . h1 . . . h2)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O x1 (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
end of H26
we proceed by induction on H26 to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex3_2_intro : x3:T x4:C H27:eq T u (lift h d x3) H28:getl O x1 (CHead x4 (Bind b) x3) H29:drop h d c1 x4 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(h1)
by (refl_equal . .)
eq T (lift h d x3) (lift h d x3)
end of h1
(h2)
by (getl_flat . . . H28 . .)
getl O (CHead x1 (Flat f) x2) (CHead x4 (Bind b) x3)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H29)
we proved
ex3_2
T
C
λv:T.λ:C.eq T (lift h d x3) (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (eq_ind_r . . . previous . H27)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (eq_ind_r . . . previous . H20)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
eq C c0 x0
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead c0 k t OF CSort ⇒c0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead x0 (Flat f) t0 OF CSort ⇒c0 | CHead c2 ⇒c2
eq C c0 x0
end of h2
by (h1 h2)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
drop h (S (plus O d)) (CHead c0 k t) e
→(drop O O (CHead c0 k t) (CHead x0 (Flat f) t0)
→(drop O O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl O e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)))
assume i0: nat
suppose IHi:
drop h (S (plus i0 d)) (CHead c0 k t) e
→(drop i0 O (CHead c0 k t) (CHead x0 (Flat f) t0)
→(drop i0 O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)))
suppose H9: drop h (S (plus (S i0) d)) (CHead c0 k t) e
suppose H10: drop (S i0) O (CHead c0 k t) (CHead x0 (Flat f) t0)
suppose IHx0:
drop (S i0) O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
by (drop_gen_skip_l . . . . . . H9)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k (plus (S i0) d)) v)
λe:C.λ:T.drop h (r k (plus (S i0) d)) c0 e
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex3_2_intro : x1:C x2:T H11:eq C e (CHead x1 k x2) H12:eq T t (lift h (r k (plus (S i0) d)) x2) H13:drop h (r k (plus (S i0) d)) c0 x1 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(H14)
by (f_equal . . . . . H12)
we proved eq T t (lift h (r k (plus (S i0) d)) x2)
eq T (λe0:T.e0 t) (λe0:T.e0 (lift h (r k (plus (S i0) d)) x2))
end of H14
(H15)
we proceed by induction on H11 to prove
drop h (S (plus i0 d)) (CHead c0 k t) (CHead x1 k x2)
→(drop i0 O (CHead c0 k t) (CHead x0 (Flat f) t0)
→(drop i0 O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)))
case refl_equal : ⇒
the thesis becomes the hypothesis IHi
drop h (S (plus i0 d)) (CHead c0 k t) (CHead x1 k x2)
→(drop i0 O (CHead c0 k t) (CHead x0 (Flat f) t0)
→(drop i0 O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)))
end of H15
(H16)
we proceed by induction on H11 to prove
drop (S i0) O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
case refl_equal : ⇒
the thesis becomes the hypothesis IHx0
drop (S i0) O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H16
(H17)
consider H14
we proved eq T t (lift h (r k (plus (S i0) d)) x2)
that is equivalent to eq T t (lift h (r k (S (plus i0 d))) x2)
we proceed by induction on the previous result to prove
drop (S i0) O (CHead c0 k (lift h (r k (S (plus i0 d))) x2)) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H16
drop (S i0) O (CHead c0 k (lift h (r k (S (plus i0 d))) x2)) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
end of H17
(H19)
by (r_plus . . .)
we proved eq nat (r k (plus (S i0) d)) (plus (r k (S i0)) d)
we proceed by induction on the previous result to prove drop h (plus (r k (S i0)) d) c0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H13
drop h (plus (r k (S i0)) d) c0 x1
end of H19
(H20)
by (r_S . .)
we proved eq nat (r k (S i0)) (S (r k i0))
we proceed by induction on the previous result to prove drop h (plus (S (r k i0)) d) c0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H19
drop h (plus (S (r k i0)) d) c0 x1
end of H20
(H21)
(h1)
(h1)
by (drop_gen_drop . . . . . H10)
drop (r k i0) O c0 (CHead x0 (Flat f) t0)
end of h1
(h2)
by (clear_gen_flat . . . . H8)
we proved clear x0 (CHead c1 (Bind b) u)
by (clear_flat . . previous . .)
clear (CHead x0 (Flat f) t0) (CHead c1 (Bind b) u)
end of h2
by (getl_intro . . . . h1 h2)
getl (r k i0) c0 (CHead c1 (Bind b) u)
end of h1
(h2)
consider H20
we proved drop h (plus (S (r k i0)) d) c0 x1
drop h (S (plus (r k i0) d)) c0 x1
end of h2
by (H . . . h1 . . . h2)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (r k i0) x1 (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
end of H21
we proceed by induction on H21 to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
case ex3_2_intro : x3:T x4:C H22:eq T u (lift h d x3) H23:getl (r k i0) x1 (CHead x4 (Bind b) x3) H24:drop h d c1 x4 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
(h1)
by (refl_equal . .)
eq T (lift h d x3) (lift h d x3)
end of h1
(h2)
by (getl_head . . . . H23 .)
getl (S i0) (CHead x1 k x2) (CHead x4 (Bind b) x3)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H24)
we proved
ex3_2
T
C
λv:T.λ:C.eq T (lift h d x3) (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (eq_ind_r . . . previous . H22)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (eq_ind_r . . . previous . H11)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
∀H9:drop h (S (plus (S i0) d)) (CHead c0 k t) e
.∀H10:drop (S i0) O (CHead c0 k t) (CHead x0 (Flat f) t0)
.∀IHx0:drop (S i0) O (CHead c0 k t) x0
→(clear x0 (CHead c1 (Bind b) u)
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0))
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl (S i0) e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (previous . H1 H7 IHx)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
∀H7:drop i O (CHead c0 k t) (CHead x0 (Flat f) t0)
.∀H8:clear (CHead x0 (Flat f) t0) (CHead c1 (Bind b) u)
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (previous . H5 H6)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
∀H5:drop i O (CHead c0 k t) (CHead x0 k0 t0)
.∀H6:clear (CHead x0 k0 t0) (CHead c1 (Bind b) u)
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
by (previous . H3 H4)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
∀c1:C
.∀u:T
.∀i:nat
.∀H0:getl i (CHead c0 k t) (CHead c1 (Bind b) u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h (S (plus i d)) (CHead c0 k t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0
we proved
∀c1:C
.∀u:T
.∀i:nat
.getl i c (CHead c1 (Bind b) u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)
we proved
∀b:B
.∀c:C
.∀c1:C
.∀u:T
.∀i:nat
.getl i c (CHead c1 (Bind b) u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h d v)
λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
λ:T.λe0:C.drop h d c1 e0)