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