DEFINITION getl_drop_trans()
TYPE =
∀c1:C
.∀c2:C
.∀h:nat
.getl h c1 c2
→∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O c1 e2)
BODY =
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀h:nat
.getl h c1 c2
→∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O c1 e2)
case CSort : n:nat ⇒
the thesis becomes
∀c2:C
.∀h:nat
.∀H:getl h (CSort n) c2
.∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O (CSort n) e2)
assume c2: C
assume h: nat
suppose H: getl h (CSort n) c2
assume e2: C
assume i: nat
suppose : drop (S i) O c2 e2
by (getl_gen_sort . . . H .)
we proved drop (S (plus i h)) O (CSort n) e2
∀c2:C
.∀h:nat
.∀H:getl h (CSort n) c2
.∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O (CSort n) e2)
case CHead ⇒
we need to prove
∀c2:C
.∀c3:C
.∀h:nat
.getl h c2 c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O c2 e2)
→∀k:K
.∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 k t) c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O (CHead c2 k t) e2)
assume c2: C
suppose IHc:
∀c3:C
.∀h:nat
.getl h c2 c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O c2 e2)
assume k: K
we proceed by induction on k to prove
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 k t) c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O (CHead c2 k t) e2)
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Bind b) t) e2
assume t: T
assume c3: C
assume h: nat
we proceed by induction on h to prove
getl h (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Bind b) t) e2
case O : ⇒
the thesis becomes
getl O (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i O)) O (CHead c2 (Bind b) t) e2
suppose H: getl O (CHead c2 (Bind b) t) c3
assume e2: C
assume i: nat
suppose H0: drop (S i) O c3 e2
(H1)
by (getl_gen_O . . H)
we proved clear (CHead c2 (Bind b) t) c3
by (clear_gen_bind . . . . previous)
we proved eq C c3 (CHead c2 (Bind b) t)
we proceed by induction on the previous result to prove drop (S i) O (CHead c2 (Bind b) t) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H0
drop (S i) O (CHead c2 (Bind b) t) e2
end of H1
by (plus_n_O .)
we proved eq nat i (plus i O)
we proceed by induction on the previous result to prove drop (S (plus i O)) O (CHead c2 (Bind b) t) e2
case refl_equal : ⇒
the thesis becomes drop (S i) O (CHead c2 (Bind b) t) e2
by (drop_gen_drop . . . . . H1)
we proved drop (r (Bind b) i) O c2 e2
by (drop_drop . . . . previous .)
drop (S i) O (CHead c2 (Bind b) t) e2
we proved drop (S (plus i O)) O (CHead c2 (Bind b) t) e2
getl O (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i O)) O (CHead c2 (Bind b) t) e2
case S : n:nat ⇒
the thesis becomes
∀H0:getl (S n) (CHead c2 (Bind b) t) c3
.∀e2:C
.∀i:nat
.∀H1:(drop (S i) O c3 e2).(drop (S (plus i (S n))) O (CHead c2 (Bind b) t) e2)
() by induction hypothesis we know
getl n (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i n)) O (CHead c2 (Bind b) t) e2
suppose H0: getl (S n) (CHead c2 (Bind b) t) c3
assume e2: C
assume i: nat
suppose H1: drop (S i) O c3 e2
by (plus_Snm_nSm . .)
we proved eq nat (plus (S i) n) (plus i (S n))
we proceed by induction on the previous result to prove drop (S (plus i (S n))) O (CHead c2 (Bind b) t) e2
case refl_equal : ⇒
the thesis becomes drop (S (plus (S i) n)) O (CHead c2 (Bind b) t) e2
by (getl_gen_S . . . . . H0)
we proved getl (r (Bind b) n) c2 c3
that is equivalent to getl n c2 c3
by (IHc . . previous . . H1)
we proved drop (S (plus i n)) O c2 e2
that is equivalent to drop (r (Bind b) (plus (S i) n)) O c2 e2
by (drop_drop . . . . previous .)
drop (S (plus (S i) n)) O (CHead c2 (Bind b) t) e2
we proved drop (S (plus i (S n))) O (CHead c2 (Bind b) t) e2
∀H0:getl (S n) (CHead c2 (Bind b) t) c3
.∀e2:C
.∀i:nat
.∀H1:(drop (S i) O c3 e2).(drop (S (plus i (S n))) O (CHead c2 (Bind b) t) e2)
we proved
getl h (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Bind b) t) e2
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 (Bind b) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Bind b) t) e2
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Flat f) t) e2
assume t: T
assume c3: C
assume h: nat
we proceed by induction on h to prove
getl h (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Flat f) t) e2
case O : ⇒
the thesis becomes
getl O (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i O)) O (CHead c2 (Flat f) t) e2
suppose H: getl O (CHead c2 (Flat f) t) c3
assume e2: C
assume i: nat
suppose H0: drop (S i) O c3 e2
(h1)
by (drop_refl .)
drop O O c2 c2
end of h1
(h2)
by (getl_gen_O . . H)
we proved clear (CHead c2 (Flat f) t) c3
by (clear_gen_flat . . . . previous)
clear c2 c3
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c2 c3
by (IHc . . previous . . H0)
we proved drop (S (plus i O)) O c2 e2
that is equivalent to drop (r (Flat f) (plus i O)) O c2 e2
by (drop_drop . . . . previous .)
we proved drop (S (plus i O)) O (CHead c2 (Flat f) t) e2
getl O (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i O)) O (CHead c2 (Flat f) t) e2
case S : n:nat ⇒
the thesis becomes
∀H0:getl (S n) (CHead c2 (Flat f) t) c3
.∀e2:C
.∀i:nat
.∀H1:(drop (S i) O c3 e2).(drop (S (plus i (S n))) O (CHead c2 (Flat f) t) e2)
() by induction hypothesis we know
getl n (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i n)) O (CHead c2 (Flat f) t) e2
suppose H0: getl (S n) (CHead c2 (Flat f) t) c3
assume e2: C
assume i: nat
suppose H1: drop (S i) O c3 e2
by (getl_gen_S . . . . . H0)
we proved getl (r (Flat f) n) c2 c3
that is equivalent to getl (S n) c2 c3
by (IHc . . previous . . H1)
we proved drop (S (plus i (S n))) O c2 e2
that is equivalent to drop (r (Flat f) (plus i (S n))) O c2 e2
by (drop_drop . . . . previous .)
we proved drop (S (plus i (S n))) O (CHead c2 (Flat f) t) e2
∀H0:getl (S n) (CHead c2 (Flat f) t) c3
.∀e2:C
.∀i:nat
.∀H1:(drop (S i) O c3 e2).(drop (S (plus i (S n))) O (CHead c2 (Flat f) t) e2)
we proved
getl h (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Flat f) t) e2
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 (Flat f) t) c3
→∀e2:C
.∀i:nat
.drop (S i) O c3 e2
→drop (S (plus i h)) O (CHead c2 (Flat f) t) e2
we proved
∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 k t) c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O (CHead c2 k t) e2)
∀c2:C
.∀c3:C
.∀h:nat
.getl h c2 c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O c2 e2)
→∀k:K
.∀t:T
.∀c3:C
.∀h:nat
.getl h (CHead c2 k t) c3
→∀e2:C.∀i:nat.(drop (S i) O c3 e2)→(drop (S (plus i h)) O (CHead c2 k t) e2)
we proved
∀c2:C
.∀h:nat
.getl h c1 c2
→∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O c1 e2)
we proved
∀c1:C
.∀c2:C
.∀h:nat
.getl h c1 c2
→∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O c1 e2)