DEFINITION drop_ctail()
TYPE =
∀c1:C
.∀c2:C
.∀d:nat.∀h:nat.(drop h d c1 c2)→∀k:K.∀u:T.(drop h d (CTail k u c1) (CTail k u c2))
BODY =
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀d:nat.∀h:nat.(drop h d c1 c2)→∀k:K.∀u:T.(drop h d (CTail k u c1) (CTail k u c2))
case CSort : n:nat ⇒
the thesis becomes
∀c2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) c2
.∀k:K.∀u:T.(drop h d (CTail k u (CSort n)) (CTail k u c2))
assume c2: C
assume d: nat
assume h: nat
suppose H: drop h d (CSort n) c2
assume k: K
assume u: T
by (drop_gen_sort . . . . H)
we proved and3 (eq C c2 (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove drop h d (CTail k u (CSort n)) (CTail k u c2)
case and3_intro : H0:eq C c2 (CSort n) H1:eq nat h O H2:eq nat d O ⇒
the thesis becomes drop h d (CTail k u (CSort n)) (CTail k u c2)
by (drop_refl .)
we proved drop O O (CTail k u (CSort n)) (CTail k u (CSort n))
by (eq_ind_r . . . previous . H0)
we proved drop O O (CTail k u (CSort n)) (CTail k u c2)
by (eq_ind_r . . . previous . H2)
we proved drop O d (CTail k u (CSort n)) (CTail k u c2)
by (eq_ind_r . . . previous . H1)
drop h d (CTail k u (CSort n)) (CTail k u c2)
we proved drop h d (CTail k u (CSort n)) (CTail k u c2)
∀c2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) c2
.∀k:K.∀u:T.(drop h d (CTail k u (CSort n)) (CTail k u c2))
case CHead : c2:C k:K t:T ⇒
the thesis becomes
∀c3:C
.∀d:nat
.∀h:nat
.drop h d (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h d (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
(IHc) by induction hypothesis we know
∀c3:C
.∀d:nat.∀h:nat.(drop h d c2 c3)→∀k:K.∀u:T.(drop h d (CTail k u c2) (CTail k u c3))
assume c3: C
assume d: nat
we proceed by induction on d to prove
∀h:nat
.drop h d (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h d (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
case O : ⇒
the thesis becomes
∀h:nat
.drop h O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
assume h: nat
we proceed by induction on h to prove
drop h O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
case O : ⇒
the thesis becomes
drop O O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
suppose H: drop O O (CHead c2 k t) c3
assume k0: K
assume u: T
by (drop_gen_refl . . H)
we proved eq C (CHead c2 k t) c3
we proceed by induction on the previous result to prove drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
case refl_equal : ⇒
the thesis becomes drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u (CHead c2 k t))
by (drop_refl .)
drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u (CHead c2 k t))
we proved drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
drop O O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
case S : n:nat ⇒
the thesis becomes
∀H0:drop (S n) O (CHead c2 k t) c3
.∀k0:K.∀u:T.(drop (S n) O (CHead (CTail k0 u c2) k t) (CTail k0 u c3))
() by induction hypothesis we know
drop n O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
suppose H0: drop (S n) O (CHead c2 k t) c3
assume k0: K
assume u: T
by (drop_gen_drop . . . . . H0)
we proved drop (r k n) O c2 c3
by (IHc . . . previous . .)
we proved drop (r k n) O (CTail k0 u c2) (CTail k0 u c3)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead (CTail k0 u c2) k t) (CTail k0 u c3)
that is equivalent to drop (S n) O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
∀H0:drop (S n) O (CHead c2 k t) c3
.∀k0:K.∀u:T.(drop (S n) O (CHead (CTail k0 u c2) k t) (CTail k0 u c3))
we proved
drop h O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
∀h:nat
.drop h O (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
case S : n:nat ⇒
the thesis becomes
∀h:nat
.∀H0:drop h (S n) (CHead c2 k t) c3
.∀k0:K.∀u:T.(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
(H) by induction hypothesis we know
∀h:nat
.drop h n (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h n (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
assume h: nat
suppose H0: drop h (S n) (CHead c2 k t) c3
assume k0: K
assume u: T
by (drop_gen_skip_l . . . . . . H0)
we proved
ex3_2
C
T
λe:C.λv:T.eq C c3 (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k n) v)
λe:C.λ:T.drop h (r k n) c2 e
we proceed by induction on the previous result to prove drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
case ex3_2_intro : x0:C x1:T H1:eq C c3 (CHead x0 k x1) H2:eq T t (lift h (r k n) x1) H3:drop h (r k n) c2 x0 ⇒
the thesis becomes drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
(H4)
we proceed by induction on H1 to prove
∀h0:nat
.drop h0 n (CHead c2 k t) (CHead x0 k x1)
→∀k1:K.∀u0:T.(drop h0 n (CTail k1 u0 (CHead c2 k t)) (CTail k1 u0 (CHead x0 k x1)))
case refl_equal : ⇒
the thesis becomes the hypothesis H
∀h0:nat
.drop h0 n (CHead c2 k t) (CHead x0 k x1)
→∀k1:K.∀u0:T.(drop h0 n (CTail k1 u0 (CHead c2 k t)) (CTail k1 u0 (CHead x0 k x1)))
end of H4
by (IHc . . . H3 . .)
we proved drop h (r k n) (CTail k0 u c2) (CTail k0 u x0)
by (drop_skip . . . . . previous .)
we proved
drop
h
S n
CHead (CTail k0 u c2) k (lift h (r k n) x1)
CHead (CTail k0 u x0) k x1
that is equivalent to
drop
h
S n
CTail k0 u (CHead c2 k (lift h (r k n) x1))
CTail k0 u (CHead x0 k x1)
by (eq_ind_r . . . previous . H2)
we proved drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u (CHead x0 k x1))
by (eq_ind_r . . . previous . H1)
drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
we proved drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)
∀h:nat
.∀H0:drop h (S n) (CHead c2 k t) c3
.∀k0:K.∀u:T.(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
we proved
∀h:nat
.drop h d (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h d (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
∀c3:C
.∀d:nat
.∀h:nat
.drop h d (CHead c2 k t) c3
→∀k0:K.∀u:T.(drop h d (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))
we proved
∀c2:C
.∀d:nat.∀h:nat.(drop h d c1 c2)→∀k:K.∀u:T.(drop h d (CTail k u c1) (CTail k u c2))
we proved
∀c1:C
.∀c2:C
.∀d:nat.∀h:nat.(drop h d c1 c2)→∀k:K.∀u:T.(drop h d (CTail k u c1) (CTail k u c2))