DEFINITION csubst0_drop_gt_back()
TYPE =
∀n:nat
.∀i:nat
.(lt i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n O c2 e)→(drop n O c1 e)
BODY =
assume n: nat
we proceed by induction on n to prove
∀i:nat
.(lt i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n O c2 e)→(drop n O c1 e)
case O : ⇒
the thesis becomes
∀i:nat
.(lt i O)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop O O c2 e)→(drop O O c1 e)
assume i: nat
suppose H: lt i O
assume c1: C
assume c2: C
assume v: T
suppose : csubst0 i v c1 c2
assume e: C
suppose : drop O O c2 e
by (lt_x_O . H .)
we proved drop O O c1 e
∀i:nat
.(lt i O)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop O O c2 e)→(drop O O c1 e)
case S : n0:nat ⇒
the thesis becomes
∀i:nat
.∀H0:lt i (S n0)
.∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O c1 e)
(H) by induction hypothesis we know ∀i:nat.(lt i n0)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n0 O c2 e)→(drop n0 O c1 e)
assume i: nat
suppose H0: lt i (S n0)
assume c1: C
we proceed by induction on c1 to prove ∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O c1 e)
case CSort : n1:nat ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀H1:(csubst0 i v (CSort n1) c2).∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O (CSort n1) e)
assume c2: C
assume v: T
suppose H1: csubst0 i v (CSort n1) c2
assume e: C
suppose : drop (S n0) O c2 e
by (csubst0_gen_sort . . . . H1 .)
we proved drop (S n0) O (CSort n1) e
∀c2:C
.∀v:T
.∀H1:(csubst0 i v (CSort n1) c2).∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O (CSort n1) e)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀H2:(csubst0 i v (CHead c k t) c2).∀e:C.∀H3:(drop (S n0) O c2 e).(drop (S n0) O (CHead c k t) e)
(H1) by induction hypothesis we know ∀c2:C.∀v:T.(csubst0 i v c c2)→∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O c e)
assume c2: C
assume v: T
suppose H2: csubst0 i v (CHead c k t) c2
assume e: C
suppose H3: drop (S n0) O c2 e
by (csubst0_gen_head . . . . . . H2)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C c2 (CHead c k u2)
λu2:T.λj:nat.subst0 j v t u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C c2 (CHead c2 k t)
λc2:C.λj:nat.csubst0 j v c c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C c2 (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v t u2
λ:T.λc2:C.λj:nat.csubst0 j v c c2
we proceed by induction on the previous result to prove drop (S n0) O (CHead c k t) e
case or3_intro0 : H4:ex3_2 T nat λ:T.λj:nat.eq nat i (s k j) λu2:T.λ:nat.eq C c2 (CHead c k u2) λu2:T.λj:nat.subst0 j v t u2 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
we proceed by induction on H4 to prove drop (S n0) O (CHead c k t) e
case ex3_2_intro : x0:T x1:nat H5:eq nat i (s k x1) H6:eq C c2 (CHead c k x0) :subst0 x1 v t x0 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
(H8)
we proceed by induction on H6 to prove drop (S n0) O (CHead c k x0) e
case refl_equal : ⇒
the thesis becomes the hypothesis H3
drop (S n0) O (CHead c k x0) e
end of H8
(H9)
we proceed by induction on H5 to prove ∀c3:C.∀v0:T.(csubst0 (s k x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀c3:C.∀v0:T.(csubst0 (s k x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
end of H9
(H10)
we proceed by induction on H5 to prove lt (s k x1) (S n0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
lt (s k x1) (S n0)
end of H10
by (drop_gen_drop . . . . . H8)
we proved drop (r k n0) O c e
assume b: B
suppose : ∀c3:C.∀v0:T.(csubst0 (s (Bind b) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose : lt (s (Bind b) x1) (S n0)
suppose H13: drop (r (Bind b) n0) O c e
by (drop_drop . . . . H13 .)
we proved drop (S n0) O (CHead c (Bind b) t) e
∀c3:C.∀v0:T.(csubst0 (s (Bind b) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
→(lt (s (Bind b) x1) (S n0)
→∀H13:(drop (r (Bind b) n0) O c e).(drop (S n0) O (CHead c (Bind b) t) e))
assume f: F
suppose : ∀c3:C.∀v0:T.(csubst0 (s (Flat f) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose H12: lt (s (Flat f) x1) (S n0)
suppose H13: drop (r (Flat f) n0) O c e
consider H12
we proved lt (s (Flat f) x1) (S n0)
that is equivalent to lt x1 (S n0)
by (lt_gen_xS . . previous)
we proved or (eq nat x1 O) (ex2 nat λm:nat.eq nat x1 (S m) λm:nat.lt m n0)
we proceed by induction on the previous result to prove drop (S n0) O (CHead c (Flat f) t) e
case or_introl : :eq nat x1 O ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
by (drop_drop . . . . H13 .)
drop (S n0) O (CHead c (Flat f) t) e
case or_intror : H14:ex2 nat λm:nat.eq nat x1 (S m) λm:nat.lt m n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
we proceed by induction on H14 to prove drop (S n0) O (CHead c (Flat f) t) e
case ex_intro2 : x:nat :eq nat x1 (S x) :lt x n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
by (drop_drop . . . . H13 .)
drop (S n0) O (CHead c (Flat f) t) e
drop (S n0) O (CHead c (Flat f) t) e
we proved drop (S n0) O (CHead c (Flat f) t) e
∀c3:C.∀v0:T.(csubst0 (s (Flat f) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
→∀H12:lt (s (Flat f) x1) (S n0)
.∀H13:(drop (r (Flat f) n0) O c e).(drop (S n0) O (CHead c (Flat f) t) e)
by (previous . H9 H10 previous)
drop (S n0) O (CHead c k t) e
drop (S n0) O (CHead c k t) e
case or3_intro1 : H4:ex3_2 C nat λ:C.λj:nat.eq nat i (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k t) λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
we proceed by induction on H4 to prove drop (S n0) O (CHead c k t) e
case ex3_2_intro : x0:C x1:nat H5:eq nat i (s k x1) H6:eq C c2 (CHead x0 k t) H7:csubst0 x1 v c x0 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
(H8)
we proceed by induction on H6 to prove drop (S n0) O (CHead x0 k t) e
case refl_equal : ⇒
the thesis becomes the hypothesis H3
drop (S n0) O (CHead x0 k t) e
end of H8
(H9)
we proceed by induction on H5 to prove ∀c3:C.∀v0:T.(csubst0 (s k x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀c3:C.∀v0:T.(csubst0 (s k x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
end of H9
(H10)
we proceed by induction on H5 to prove lt (s k x1) (S n0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
lt (s k x1) (S n0)
end of H10
by (drop_gen_drop . . . . . H8)
we proved drop (r k n0) O x0 e
assume b: B
suppose : ∀c3:C.∀v0:T.(csubst0 (s (Bind b) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose H12: lt (s (Bind b) x1) (S n0)
suppose H13: drop (r (Bind b) n0) O x0 e
(h1)
consider H12
we proved lt (s (Bind b) x1) (S n0)
that is equivalent to lt (S x1) (S n0)
by (lt_S_n . . previous)
lt x1 n0
end of h1
(h2)
consider H13
we proved drop (r (Bind b) n0) O x0 e
drop n0 O x0 e
end of h2
by (H . h1 . . . H7 . h2)
we proved drop n0 O c e
that is equivalent to drop (r (Bind b) n0) O c e
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) e
∀c3:C.∀v0:T.(csubst0 (s (Bind b) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
→∀H12:lt (s (Bind b) x1) (S n0)
.∀H13:(drop (r (Bind b) n0) O x0 e).(drop (S n0) O (CHead c (Bind b) t) e)
assume f: F
suppose H11: ∀c3:C.∀v0:T.(csubst0 (s (Flat f) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose H12: lt (s (Flat f) x1) (S n0)
suppose H13: drop (r (Flat f) n0) O x0 e
consider H12
we proved lt (s (Flat f) x1) (S n0)
that is equivalent to lt x1 (S n0)
by (lt_gen_xS . . previous)
we proved or (eq nat x1 O) (ex2 nat λm:nat.eq nat x1 (S m) λm:nat.lt m n0)
we proceed by induction on the previous result to prove drop (S n0) O (CHead c (Flat f) t) e
case or_introl : :eq nat x1 O ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
(h1)
consider H7
we proved csubst0 x1 v c x0
csubst0 (s (Flat f) x1) v c x0
end of h1
(h2)
consider H13
we proved drop (r (Flat f) n0) O x0 e
drop (S n0) O x0 e
end of h2
by (H11 . . h1 . h2)
we proved drop (S n0) O c e
that is equivalent to drop (r (Flat f) n0) O c e
by (drop_drop . . . . previous .)
drop (S n0) O (CHead c (Flat f) t) e
case or_intror : H14:ex2 nat λm:nat.eq nat x1 (S m) λm:nat.lt m n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
we proceed by induction on H14 to prove drop (S n0) O (CHead c (Flat f) t) e
case ex_intro2 : x:nat :eq nat x1 (S x) :lt x n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
(h1)
consider H7
we proved csubst0 x1 v c x0
csubst0 (s (Flat f) x1) v c x0
end of h1
(h2)
consider H13
we proved drop (r (Flat f) n0) O x0 e
drop (S n0) O x0 e
end of h2
by (H11 . . h1 . h2)
we proved drop (S n0) O c e
that is equivalent to drop (r (Flat f) n0) O c e
by (drop_drop . . . . previous .)
drop (S n0) O (CHead c (Flat f) t) e
drop (S n0) O (CHead c (Flat f) t) e
we proved drop (S n0) O (CHead c (Flat f) t) e
∀H11:∀c3:C.∀v0:T.(csubst0 (s (Flat f) x1) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
.∀H12:lt (s (Flat f) x1) (S n0)
.∀H13:(drop (r (Flat f) n0) O x0 e).(drop (S n0) O (CHead c (Flat f) t) e)
by (previous . H9 H10 previous)
drop (S n0) O (CHead c k t) e
drop (S n0) O (CHead c k t) e
case or3_intro2 : H4:ex4_3 T C nat λ:T.λ:C.λj:nat.eq nat i (s k j) λu2:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u2) λu2:T.λ:C.λj:nat.subst0 j v t u2 λ:T.λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
we proceed by induction on H4 to prove drop (S n0) O (CHead c k t) e
case ex4_3_intro : x0:T x1:C x2:nat H5:eq nat i (s k x2) H6:eq C c2 (CHead x1 k x0) :subst0 x2 v t x0 H8:csubst0 x2 v c x1 ⇒
the thesis becomes drop (S n0) O (CHead c k t) e
(H9)
we proceed by induction on H6 to prove drop (S n0) O (CHead x1 k x0) e
case refl_equal : ⇒
the thesis becomes the hypothesis H3
drop (S n0) O (CHead x1 k x0) e
end of H9
(H10)
we proceed by induction on H5 to prove ∀c3:C.∀v0:T.(csubst0 (s k x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀c3:C.∀v0:T.(csubst0 (s k x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
end of H10
(H11)
we proceed by induction on H5 to prove lt (s k x2) (S n0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
lt (s k x2) (S n0)
end of H11
by (drop_gen_drop . . . . . H9)
we proved drop (r k n0) O x1 e
assume b: B
suppose : ∀c3:C.∀v0:T.(csubst0 (s (Bind b) x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose H13: lt (s (Bind b) x2) (S n0)
suppose H14: drop (r (Bind b) n0) O x1 e
(h1)
consider H13
we proved lt (s (Bind b) x2) (S n0)
that is equivalent to lt (S x2) (S n0)
by (lt_S_n . . previous)
lt x2 n0
end of h1
(h2)
consider H14
we proved drop (r (Bind b) n0) O x1 e
drop n0 O x1 e
end of h2
by (H . h1 . . . H8 . h2)
we proved drop n0 O c e
that is equivalent to drop (r (Bind b) n0) O c e
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) e
∀c3:C.∀v0:T.(csubst0 (s (Bind b) x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
→∀H13:lt (s (Bind b) x2) (S n0)
.∀H14:(drop (r (Bind b) n0) O x1 e).(drop (S n0) O (CHead c (Bind b) t) e)
assume f: F
suppose H12: ∀c3:C.∀v0:T.(csubst0 (s (Flat f) x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
suppose H13: lt (s (Flat f) x2) (S n0)
suppose H14: drop (r (Flat f) n0) O x1 e
consider H13
we proved lt (s (Flat f) x2) (S n0)
that is equivalent to lt x2 (S n0)
by (lt_gen_xS . . previous)
we proved or (eq nat x2 O) (ex2 nat λm:nat.eq nat x2 (S m) λm:nat.lt m n0)
we proceed by induction on the previous result to prove drop (S n0) O (CHead c (Flat f) t) e
case or_introl : :eq nat x2 O ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
(h1)
consider H8
we proved csubst0 x2 v c x1
csubst0 (s (Flat f) x2) v c x1
end of h1
(h2)
consider H14
we proved drop (r (Flat f) n0) O x1 e
drop (S n0) O x1 e
end of h2
by (H12 . . h1 . h2)
we proved drop (S n0) O c e
that is equivalent to drop (r (Flat f) n0) O c e
by (drop_drop . . . . previous .)
drop (S n0) O (CHead c (Flat f) t) e
case or_intror : H15:ex2 nat λm:nat.eq nat x2 (S m) λm:nat.lt m n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
we proceed by induction on H15 to prove drop (S n0) O (CHead c (Flat f) t) e
case ex_intro2 : x:nat :eq nat x2 (S x) :lt x n0 ⇒
the thesis becomes drop (S n0) O (CHead c (Flat f) t) e
(h1)
consider H8
we proved csubst0 x2 v c x1
csubst0 (s (Flat f) x2) v c x1
end of h1
(h2)
consider H14
we proved drop (r (Flat f) n0) O x1 e
drop (S n0) O x1 e
end of h2
by (H12 . . h1 . h2)
we proved drop (S n0) O c e
that is equivalent to drop (r (Flat f) n0) O c e
by (drop_drop . . . . previous .)
drop (S n0) O (CHead c (Flat f) t) e
drop (S n0) O (CHead c (Flat f) t) e
we proved drop (S n0) O (CHead c (Flat f) t) e
∀H12:∀c3:C.∀v0:T.(csubst0 (s (Flat f) x2) v0 c c3)→∀e0:C.(drop (S n0) O c3 e0)→(drop (S n0) O c e0)
.∀H13:lt (s (Flat f) x2) (S n0)
.∀H14:(drop (r (Flat f) n0) O x1 e).(drop (S n0) O (CHead c (Flat f) t) e)
by (previous . H10 H11 previous)
drop (S n0) O (CHead c k t) e
drop (S n0) O (CHead c k t) e
we proved drop (S n0) O (CHead c k t) e
∀c2:C
.∀v:T
.∀H2:(csubst0 i v (CHead c k t) c2).∀e:C.∀H3:(drop (S n0) O c2 e).(drop (S n0) O (CHead c k t) e)
we proved ∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O c1 e)
∀i:nat
.∀H0:lt i (S n0)
.∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop (S n0) O c2 e)→(drop (S n0) O c1 e)
we proved
∀i:nat
.(lt i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n O c2 e)→(drop n O c1 e)
we proved
∀n:nat
.∀i:nat
.(lt i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n O c2 e)→(drop n O c1 e)