DEFINITION drop_conf_lt()
TYPE =
∀k:K
.∀i:nat
.∀u:T
.∀c0:C
.∀c:C
.drop i O c (CHead c0 k 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 (r k d) v)
λv:T.λe0:C.drop i O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
BODY =
assume k: K
assume i: nat
we proceed by induction on i to prove
∀u:T
.∀c0:C
.∀c:C
.drop i O c (CHead c0 k 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 (r k d) v)
λv:T.λe0:C.drop i O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
case O : ⇒
the thesis becomes
∀u:T
.∀c0:C
.∀c:C
.drop O O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus O d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
assume u: T
assume c0: C
assume c: C
suppose H: drop O O c (CHead c0 k u)
assume e: C
assume h: nat
assume d: nat
suppose H0: drop h (S (plus O d)) c e
(H1)
by (drop_gen_refl . . H)
we proved eq C c (CHead c0 k u)
we proceed by induction on the previous result to prove drop h (S (plus O d)) (CHead c0 k u) e
case refl_equal : ⇒
the thesis becomes the hypothesis H0
drop h (S (plus O d)) (CHead c0 k u) e
end of H1
by (drop_gen_skip_l . . . . . . H1)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k (plus O d)) v)
λe:C.λ:T.drop h (r k (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 (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case ex3_2_intro : x0:C x1:T H2:eq C e (CHead x0 k x1) H3:eq T u (lift h (r k (plus O d)) x1) H4:drop h (r k (plus O d)) c0 x0 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
(h1)
by (refl_equal . .)
we proved eq T (lift h (r k d) x1) (lift h (r k d) x1)
eq T (lift h (r k (plus O d)) x1) (lift h (r k d) x1)
end of h1
(h2)
by (drop_refl .)
drop O O (CHead x0 k x1) (CHead x0 k x1)
end of h2
(h3)
consider H4
we proved drop h (r k (plus O d)) c0 x0
drop h (r k d) c0 x0
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
C
λv:T.λ:C.eq T (lift h (r k (plus O d)) x1) (lift h (r k d) v)
λv:T.λe0:C.drop O O (CHead x0 k x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
by (eq_ind_r . . . previous . H3)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O (CHead x0 k x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
by (eq_ind_r . . . previous . H2)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
∀u:T
.∀c0:C
.∀c:C
.drop O O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus O d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop O O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
case S : i0:nat ⇒
the thesis becomes
∀u:T
.∀c0:C
.∀c:C
.drop (S i0) O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
(H) by induction hypothesis we know
∀u:T
.∀c0:C
.∀c:C
.drop i0 O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus i0 d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop i0 O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
assume u: T
assume c0: C
assume c: C
we proceed by induction on c to prove
drop (S i0) O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
case CSort : n:nat ⇒
the thesis becomes
drop (S i0) O (CSort n) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h (S (plus (S i0) d)) (CSort n) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
suppose : drop (S i0) O (CSort n) (CHead c0 k u)
assume e: C
assume h: nat
assume d: nat
suppose H1: drop h (S (plus (S i0) d)) (CSort n) e
by (drop_gen_sort . . . . H1)
we proved and3 (eq C e (CSort n)) (eq nat h O) (eq nat (S (plus (S i0) d)) O)
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case and3_intro : :eq C e (CSort n) :eq nat h O H4:eq nat (S (plus (S i0) d)) O ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
(H5)
we proceed by induction on H4 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S (plus (S i0) d) OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S (plus (S i0) d) OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H5
consider H5
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
drop (S i0) O (CSort n) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h (S (plus (S i0) d)) (CSort n) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case CHead ⇒
we need to prove
∀c1:C
.drop (S i0) O c1 (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c1 e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
→∀k0:K
.∀t:T
.drop (S i0) O (CHead c1 k0 t) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) (CHead c1 k0 t) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
assume c1: C
suppose H0:
drop (S i0) O c1 (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c1 e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
assume k0: K
we proceed by induction on k0 to prove
∀t:T
.drop (S i0) O (CHead c1 k0 t) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) (CHead c1 k0 t) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀H1:drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h (S (plus (S i0) d)) (CHead c1 (Bind b) t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
assume t: T
suppose H1: drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u)
assume e: C
assume h: nat
assume d: nat
suppose H2: drop h (S (plus (S i0) d)) (CHead c1 (Bind b) t) e
by (drop_gen_skip_l . . . . . . H2)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e (Bind b) v)
λ:C.λv:T.eq T t (lift h (r (Bind b) (plus (S i0) d)) v)
λe:C.λ:T.drop h (r (Bind b) (plus (S i0) d)) c1 e
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case ex3_2_intro : x0:C x1:T H3:eq C e (CHead x0 (Bind b) x1) :eq T t (lift h (r (Bind b) (plus (S i0) d)) x1) H5:drop h (r (Bind b) (plus (S i0) d)) c1 x0 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
(H6)
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Bind b) i0) O c1 (CHead c0 k u)
drop i0 O c1 (CHead c0 k u)
end of h1
(h2)
consider H5
we proved drop h (r (Bind b) (plus (S i0) d)) c1 x0
drop h (S (plus i0 d)) c1 x0
end of h2
by (H . . . h1 . . . h2)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop i0 O x0 (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
end of H6
we proceed by induction on H6 to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case ex3_2_intro : x2:T x3:C H7:eq T u (lift h (r k d) x2) H8:drop i0 O x0 (CHead x3 k x2) H9:drop h (r k d) c0 x3 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
consider H8
we proved drop i0 O x0 (CHead x3 k x2)
that is equivalent to drop (r (Bind b) i0) O x0 (CHead x3 k x2)
by (drop_drop . . . . previous .)
we proved drop (S i0) O (CHead x0 (Bind b) x1) (CHead x3 k x2)
by (ex3_2_intro . . . . . . . H7 previous H9)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
by (eq_ind_r . . . previous . H3)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
∀t:T
.∀H1:drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h (S (plus (S i0) d)) (CHead c1 (Bind b) t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀H1:drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
assume t: T
suppose H1: drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u)
assume e: C
assume h: nat
assume d: nat
suppose H2: drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t) e
by (drop_gen_skip_l . . . . . . H2)
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 (S i0) d)) v)
λe:C.λ:T.drop h (r (Flat f) (plus (S i0) d)) c1 e
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case ex3_2_intro : x0:C x1:T H3:eq C e (CHead x0 (Flat f) x1) :eq T t (lift h (r (Flat f) (plus (S i0) d)) x1) H5:drop h (r (Flat f) (plus (S i0) d)) c1 x0 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Flat f) i0) O c1 (CHead c0 k u)
drop (S i0) O c1 (CHead c0 k u)
end of h1
(h2)
consider H5
we proved drop h (r (Flat f) (plus (S i0) d)) c1 x0
drop h (S (plus (S i0) d)) c1 x0
end of h2
by (H0 h1 . . . h2)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O x0 (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proceed by induction on the previous result to prove
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
case ex3_2_intro : x2:T x3:C H6:eq T u (lift h (r k d) x2) H7:drop (S i0) O x0 (CHead x3 k x2) H8:drop h (r k d) c0 x3 ⇒
the thesis becomes
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
consider H7
we proved drop (S i0) O x0 (CHead x3 k x2)
that is equivalent to drop (r (Flat f) i0) O x0 (CHead x3 k x2)
by (drop_drop . . . . previous .)
we proved drop (S i0) O (CHead x0 (Flat f) x1) (CHead x3 k x2)
by (ex3_2_intro . . . . . . . H6 previous H8)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
by (eq_ind_r . . . previous . H3)
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
∀t:T
.∀H1:drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u)
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t) e
.ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0
we proved
∀t:T
.drop (S i0) O (CHead c1 k0 t) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) (CHead c1 k0 t) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
∀c1:C
.drop (S i0) O c1 (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c1 e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
→∀k0:K
.∀t:T
.drop (S i0) O (CHead c1 k0 t) (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) (CHead c1 k0 t) e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
we proved
drop (S i0) O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
∀u:T
.∀c0:C
.∀c:C
.drop (S i0) O c (CHead c0 k u)
→∀e:C
.∀h:nat
.∀d:nat
.drop h (S (plus (S i0) d)) c e
→(ex3_2
T
C
λv:T.λ:C.eq T u (lift h (r k d) v)
λv:T.λe0:C.drop (S i0) O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
we proved
∀u:T
.∀c0:C
.∀c:C
.drop i O c (CHead c0 k 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 (r k d) v)
λv:T.λe0:C.drop i O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)
we proved
∀k:K
.∀i:nat
.∀u:T
.∀c0:C
.∀c:C
.drop i O c (CHead c0 k 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 (r k d) v)
λv:T.λe0:C.drop i O e (CHead e0 k v)
λ:T.λe0:C.drop h (r k d) c0 e0)