DEFINITION drop_conf_rev()
TYPE =
∀j:nat
.∀e1:C
.∀e2:C
.drop j O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j O c1 c2 λc1:C.drop i j c1 e1)
BODY =
assume j: nat
we proceed by induction on j to prove
∀e1:C
.∀e2:C
.drop j O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j O c1 c2 λc1:C.drop i j c1 e1)
case O : ⇒
the thesis becomes
∀e1:C
.∀e2:C
.drop O O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop O O c1 c2 λc1:C.drop i O c1 e1)
assume e1: C
assume e2: C
suppose H: drop O O e1 e2
assume c2: C
assume i: nat
suppose H0: drop i O c2 e2
(H1)
by (drop_gen_refl . . H)
we proved eq C e1 e2
by (eq_ind_r . . . H0 . previous)
drop i O c2 e1
end of H1
by (drop_refl .)
we proved drop O O c2 c2
by (ex_intro2 . . . . previous H1)
we proved ex2 C λc1:C.drop O O c1 c2 λc1:C.drop i O c1 e1
∀e1:C
.∀e2:C
.drop O O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop O O c1 c2 λc1:C.drop i O c1 e1)
case S : j0:nat ⇒
the thesis becomes
∀e1:C
.∀e2:C
.drop (S j0) O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e1)
(IHj) by induction hypothesis we know
∀e1:C
.∀e2:C.(drop j0 O e1 e2)→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j0 O c1 c2 λc1:C.drop i j0 c1 e1)
assume e1: C
we proceed by induction on e1 to prove
∀e2:C
.drop (S j0) O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e1)
case CSort : n:nat ⇒
the thesis becomes
∀e2:C
.∀H:drop (S j0) O (CSort n) e2
.∀c2:C.∀i:nat.∀H0:(drop i O c2 e2).(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n))
assume e2: C
suppose H: drop (S j0) O (CSort n) e2
assume c2: C
assume i: nat
suppose H0: drop i O c2 e2
by (drop_gen_sort . . . . H)
we proved and3 (eq C e2 (CSort n)) (eq nat (S j0) O) (eq nat O O)
we proceed by induction on the previous result to prove ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n)
case and3_intro : H1:eq C e2 (CSort n) H2:eq nat (S j0) O :eq nat O O ⇒
the thesis becomes ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n)
(H5)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S j0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S j0 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 ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n)
ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n)
we proved ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n)
∀e2:C
.∀H:drop (S j0) O (CSort n) e2
.∀c2:C.∀i:nat.∀H0:(drop i O c2 e2).(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CSort n))
case CHead : e2:C k:K t:T ⇒
the thesis becomes
∀e3:C
.∀H:drop (S j0) O (CHead e2 k t) e3
.∀c2:C.∀i:nat.∀H0:(drop i O c2 e3).(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 k t))
(IHe1) by induction hypothesis we know
∀e3:C
.drop (S j0) O e2 e3
→∀c2:C.∀i:nat.(drop i O c2 e3)→(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e2)
assume e3: C
suppose H: drop (S j0) O (CHead e2 k t) e3
assume c2: C
assume i: nat
suppose H0: drop i O c2 e3
by (drop_gen_drop . . . . . H)
we proved drop (r k j0) O e2 e3
assume b: B
suppose H1: drop (r (Bind b) j0) O e2 e3
(H_x)
consider H1
we proved drop (r (Bind b) j0) O e2 e3
that is equivalent to drop j0 O e2 e3
by (IHj . . previous . . H0)
ex2 C λc1:C.drop j0 O c1 c2 λc1:C.drop i j0 c1 e2
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Bind b) t)
case ex_intro2 : x:C H3:drop j0 O x c2 H4:drop i j0 x e2 ⇒
the thesis becomes ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Bind b) t)
(h1)
consider H3
we proved drop j0 O x c2
that is equivalent to drop (r (Bind b) j0) O x c2
by (drop_drop . . . . previous .)
drop (S j0) O (CHead x (Bind b) (lift i (r (Bind b) j0) t)) c2
end of h1
(h2)
consider H4
we proved drop i j0 x e2
that is equivalent to drop i (r (Bind b) j0) x e2
by (drop_skip . . . . . previous .)
drop
i
S j0
CHead x (Bind b) (lift i (r (Bind b) j0) t)
CHead e2 (Bind b) t
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Bind b) t)
we proved ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Bind b) t)
∀H1:drop (r (Bind b) j0) O e2 e3
.ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Bind b) t)
assume f: F
suppose H1: drop (r (Flat f) j0) O e2 e3
(H_x)
consider H1
we proved drop (r (Flat f) j0) O e2 e3
that is equivalent to drop (S j0) O e2 e3
by (IHe1 . previous . . H0)
ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e2
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Flat f) t)
case ex_intro2 : x:C H3:drop (S j0) O x c2 H4:drop i (S j0) x e2 ⇒
the thesis becomes ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Flat f) t)
(h1)
consider H3
we proved drop (S j0) O x c2
that is equivalent to drop (r (Flat f) j0) O x c2
by (drop_drop . . . . previous .)
drop (S j0) O (CHead x (Flat f) (lift i (r (Flat f) j0) t)) c2
end of h1
(h2)
consider H4
we proved drop i (S j0) x e2
that is equivalent to drop i (r (Flat f) j0) x e2
by (drop_skip . . . . . previous .)
drop
i
S j0
CHead x (Flat f) (lift i (r (Flat f) j0) t)
CHead e2 (Flat f) t
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Flat f) t)
we proved ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Flat f) t)
∀H1:drop (r (Flat f) j0) O e2 e3
.ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 (Flat f) t)
by (previous . previous)
we proved ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 k t)
∀e3:C
.∀H:drop (S j0) O (CHead e2 k t) e3
.∀c2:C.∀i:nat.∀H0:(drop i O c2 e3).(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 (CHead e2 k t))
we proved
∀e2:C
.drop (S j0) O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e1)
∀e1:C
.∀e2:C
.drop (S j0) O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop (S j0) O c1 c2 λc1:C.drop i (S j0) c1 e1)
we proved
∀e1:C
.∀e2:C
.drop j O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j O c1 c2 λc1:C.drop i j c1 e1)
we proved
∀j:nat
.∀e1:C
.∀e2:C
.drop j O e1 e2
→∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j O c1 c2 λc1:C.drop i j c1 e1)