DEFINITION csubst0_drop_lt_back()
TYPE =
∀n:nat
.∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop n O c2 e2
→or (drop n O c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.drop n O c1 e1)
BODY =
assume n: nat
we proceed by induction on n to prove
∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop n O c2 e2
→or (drop n O c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.drop n O c1 e1)
case O : ⇒
the thesis becomes
∀i:nat
.lt O i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop O O c2 e2
→or (drop O O c1 e2) (ex2 C λe1:C.csubst0 (minus i O) v e1 e2 λe1:C.drop O O c1 e1)
assume i: nat
suppose : lt O i
assume c1: C
assume c2: C
assume v: T
suppose H0: csubst0 i v c1 c2
assume e2: C
suppose H1: drop O O c2 e2
by (drop_gen_refl . . H1)
we proved eq C c2 e2
we proceed by induction on the previous result to prove or (drop O O c1 e2) (ex2 C λe1:C.csubst0 (minus i O) v e1 e2 λe1:C.drop O O c1 e1)
case refl_equal : ⇒
the thesis becomes or (drop O O c1 c2) (ex2 C λe1:C.csubst0 (minus i O) v e1 c2 λe1:C.drop O O c1 e1)
by (minus_n_O .)
we proved eq nat i (minus i O)
we proceed by induction on the previous result to prove or (drop O O c1 c2) (ex2 C λe1:C.csubst0 (minus i O) v e1 c2 λe1:C.drop O O c1 e1)
case refl_equal : ⇒
the thesis becomes or (drop O O c1 c2) (ex2 C λe1:C.csubst0 i v e1 c2 λe1:C.drop O O c1 e1)
by (drop_refl .)
we proved drop O O c1 c1
by (ex_intro2 . . . . H0 previous)
we proved ex2 C λe1:C.csubst0 i v e1 c2 λe1:C.drop O O c1 e1
by (or_intror . . previous)
or (drop O O c1 c2) (ex2 C λe1:C.csubst0 i v e1 c2 λe1:C.drop O O c1 e1)
or (drop O O c1 c2) (ex2 C λe1:C.csubst0 (minus i O) v e1 c2 λe1:C.drop O O c1 e1)
we proved or (drop O O c1 e2) (ex2 C λe1:C.csubst0 (minus i O) v e1 e2 λe1:C.drop O O c1 e1)
∀i:nat
.lt O i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop O O c2 e2
→or (drop O O c1 e2) (ex2 C λe1:C.csubst0 (minus i O) v e1 e2 λe1:C.drop O O c1 e1)
case S : n0:nat ⇒
the thesis becomes
∀i:nat
.∀H:lt (S n0) i
.∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop (S n0) O c2 e2
→or (drop (S n0) O c1 e2) (ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O c1 e1)
(IHn) by induction hypothesis we know
∀i:nat
.lt n0 i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C.(drop n0 O c2 e2)→(or (drop n0 O c1 e2) (ex2 C λe1:C.csubst0 (minus i n0) v e1 e2 λe1:C.drop n0 O c1 e1))
assume i: nat
suppose H: lt (S n0) i
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop (S n0) O c2 e2
→or (drop (S n0) O c1 e2) (ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O c1 e1)
case CSort : n1:nat ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀H0:csubst0 i v (CSort n1) c2
.∀e2:C
.drop (S n0) O c2 e2
→(or
drop (S n0) O (CSort n1) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CSort n1) e1)
assume c2: C
assume v: T
suppose H0: csubst0 i v (CSort n1) c2
assume e2: C
suppose : drop (S n0) O c2 e2
by (csubst0_gen_sort . . . . H0 .)
we proved
or
drop (S n0) O (CSort n1) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CSort n1) e1
∀c2:C
.∀v:T
.∀H0:csubst0 i v (CSort n1) c2
.∀e2:C
.drop (S n0) O c2 e2
→(or
drop (S n0) O (CSort n1) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CSort n1) e1)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀H1:csubst0 i v (CHead c k t) c2
.∀e2:C
.∀H2:drop (S n0) O c2 e2
.or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
(H0) by induction hypothesis we know
∀c2:C
.∀v:T
.csubst0 i v c c2
→∀e2:C
.drop (S n0) O c2 e2
→or (drop (S n0) O c e2) (ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1)
assume c2: C
assume v: T
suppose H1: csubst0 i v (CHead c k t) c2
assume e2: C
suppose H2: drop (S n0) O c2 e2
by (csubst0_gen_head . . . . . . H1)
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
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case or3_intro0 : H3: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
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
we proceed by induction on H3 to prove
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case ex3_2_intro : x0:T x1:nat H4:eq nat i (s k x1) H5:eq C c2 (CHead c k x0) :subst0 x1 v t x0 ⇒
the thesis becomes
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
(H7)
we proceed by induction on H5 to prove drop (S n0) O (CHead c k x0) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop (S n0) O (CHead c k x0) e2
end of H7
(H8)
we proceed by induction on H4 to prove
∀c3:C
.∀v0:T
.csubst0 (s k x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀c3:C
.∀v0:T
.csubst0 (s k x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
end of H8
(H9)
we proceed by induction on H4 to prove lt (S n0) (s k x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H
lt (S n0) (s k x1)
end of H9
by (drop_gen_drop . . . . . H7)
we proved drop (r k n0) O c e2
assume b: B
suppose :
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose : lt (S n0) (s (Bind b) x1)
suppose H12: drop (r (Bind b) n0) O c e2
by (drop_drop . . . . H12 .)
we proved drop (S n0) O (CHead c (Bind b) t) e2
by (or_introl . . previous)
we proved
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
→(lt (S n0) (s (Bind b) x1)
→∀H12:drop (r (Bind b) n0) O c e2
.or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1)
assume f: F
suppose :
∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose : lt (S n0) (s (Flat f) x1)
suppose H12: drop (r (Flat f) n0) O c e2
by (drop_drop . . . . H12 .)
we proved drop (S n0) O (CHead c (Flat f) t) e2
by (or_introl . . previous)
we proved
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
→(lt (S n0) (s (Flat f) x1)
→∀H12:drop (r (Flat f) n0) O c e2
.or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1)
by (previous . H8 H9 previous)
we proved
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
by (eq_ind_r . . . previous . H4)
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case or3_intro1 : H3: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
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
we proceed by induction on H3 to prove
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case ex3_2_intro : x0:C x1:nat H4:eq nat i (s k x1) H5:eq C c2 (CHead x0 k t) H6:csubst0 x1 v c x0 ⇒
the thesis becomes
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
(H7)
we proceed by induction on H5 to prove drop (S n0) O (CHead x0 k t) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop (S n0) O (CHead x0 k t) e2
end of H7
(H8)
we proceed by induction on H4 to prove
∀c3:C
.∀v0:T
.csubst0 (s k x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀c3:C
.∀v0:T
.csubst0 (s k x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
end of H8
(H9)
we proceed by induction on H4 to prove lt (S n0) (s k x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H
lt (S n0) (s k x1)
end of H9
by (drop_gen_drop . . . . . H7)
we proved drop (r k n0) O x0 e2
assume b: B
suppose :
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose H11: lt (S n0) (s (Bind b) x1)
suppose H12: drop (r (Bind b) n0) O x0 e2
(H_x)
(h1)
consider H11
we proved lt (S n0) (s (Bind b) x1)
that is equivalent to lt (S n0) (S x1)
by (lt_S_n . . previous)
lt n0 x1
end of h1
(h2)
consider H12
we proved drop (r (Bind b) n0) O x0 e2
drop n0 O x0 e2
end of h2
by (IHn . h1 . . . H6 . h2)
or (drop n0 O c e2) (ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop n0 O c e1)
end of H_x
(H13) consider H_x
we proceed by induction on H13 to prove
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case or_introl : H14:drop n0 O c e2 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
consider H14
we proved drop n0 O c e2
that is equivalent to drop (r (Bind b) n0) O c e2
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) e2
by (or_introl . . previous)
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case or_intror : H14:ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop n0 O c e1 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
we proceed by induction on H14 to prove
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case ex_intro2 : x:C H15:csubst0 (minus x1 n0) v x e2 H16:drop n0 O c x ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
consider H16
we proved drop n0 O c x
that is equivalent to drop (r (Bind b) n0) O c x
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) x
by (ex_intro2 . . . . H15 previous)
we proved ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
by (or_intror . . previous)
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
we proved
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
→∀H11:lt (S n0) (s (Bind b) x1)
.∀H12:drop (r (Bind b) n0) O x0 e2
.or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x1 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
assume f: F
suppose H10:
∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose : lt (S n0) (s (Flat f) x1)
suppose H12: drop (r (Flat f) n0) O x0 e2
(H_x)
(h1)
consider H6
we proved csubst0 x1 v c x0
csubst0 (s (Flat f) x1) v c x0
end of h1
(h2)
consider H12
we proved drop (r (Flat f) n0) O x0 e2
drop (S n0) O x0 e2
end of h2
by (H10 . . h1 . h2)
or
drop (S n0) O c e2
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1
end of H_x
(H13) consider H_x
consider H13
we proved
or
drop (S n0) O c e2
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1
that is equivalent to or (drop (S n0) O c e2) (ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1)
we proceed by induction on the previous result to prove
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case or_introl : H14:drop (S n0) O c e2 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
consider H14
we proved drop (S n0) O c e2
that is equivalent to drop (r (Flat f) n0) O c e2
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Flat f) t) e2
by (or_introl . . previous)
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case or_intror : H14:ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
we proceed by induction on H14 to prove
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case ex_intro2 : x:C H15:csubst0 (minus x1 (S n0)) v x e2 H16:drop (S n0) O c x ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
consider H16
we proved drop (S n0) O c x
that is equivalent to drop (r (Flat f) n0) O c x
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Flat f) t) x
by (ex_intro2 . . . . H15 previous)
we proved ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
by (or_intror . . previous)
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
we proved
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
∀H10:∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x1) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x1) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
.lt (S n0) (s (Flat f) x1)
→∀H12:drop (r (Flat f) n0) O x0 e2
.or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x1 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
by (previous . H8 H9 previous)
we proved
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus (s k x1) (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
by (eq_ind_r . . . previous . H4)
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case or3_intro2 : H3: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
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
we proceed by induction on H3 to prove
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
case ex4_3_intro : x0:T x1:C x2:nat H4:eq nat i (s k x2) H5:eq C c2 (CHead x1 k x0) :subst0 x2 v t x0 H7:csubst0 x2 v c x1 ⇒
the thesis becomes
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
(H8)
we proceed by induction on H5 to prove drop (S n0) O (CHead x1 k x0) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop (S n0) O (CHead x1 k x0) e2
end of H8
(H9)
we proceed by induction on H4 to prove
∀c3:C
.∀v0:T
.csubst0 (s k x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀c3:C
.∀v0:T
.csubst0 (s k x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s k x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
end of H9
(H10)
we proceed by induction on H4 to prove lt (S n0) (s k x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H
lt (S n0) (s k x2)
end of H10
by (drop_gen_drop . . . . . H8)
we proved drop (r k n0) O x1 e2
assume b: B
suppose :
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose H12: lt (S n0) (s (Bind b) x2)
suppose H13: drop (r (Bind b) n0) O x1 e2
(H_x)
(h1)
consider H12
we proved lt (S n0) (s (Bind b) x2)
that is equivalent to lt (S n0) (S x2)
by (lt_S_n . . previous)
lt n0 x2
end of h1
(h2)
consider H13
we proved drop (r (Bind b) n0) O x1 e2
drop n0 O x1 e2
end of h2
by (IHn . h1 . . . H7 . h2)
or (drop n0 O c e2) (ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop n0 O c e1)
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case or_introl : H15:drop n0 O c e2 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
consider H15
we proved drop n0 O c e2
that is equivalent to drop (r (Bind b) n0) O c e2
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) e2
by (or_introl . . previous)
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case or_intror : H15:ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop n0 O c e1 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
we proceed by induction on H15 to prove
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
case ex_intro2 : x:C H16:csubst0 (minus x2 n0) v x e2 H17:drop n0 O c x ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
consider H17
we proved drop n0 O c x
that is equivalent to drop (r (Bind b) n0) O c x
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Bind b) t) x
by (ex_intro2 . . . . H16 previous)
we proved ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
by (or_intror . . previous)
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
we proved
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Bind b) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Bind b) x2) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
∀c3:C
.∀v0:T
.csubst0 (s (Bind b) x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Bind b) x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
→∀H12:lt (S n0) (s (Bind b) x2)
.∀H13:drop (r (Bind b) n0) O x1 e2
.or
drop (S n0) O (CHead c (Bind b) t) e2
ex2 C λe1:C.csubst0 (minus x2 n0) v e1 e2 λe1:C.drop (S n0) O (CHead c (Bind b) t) e1
assume f: F
suppose H11:
∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
suppose : lt (S n0) (s (Flat f) x2)
suppose H13: drop (r (Flat f) n0) O x1 e2
(H_x)
(h1)
consider H7
we proved csubst0 x2 v c x1
csubst0 (s (Flat f) x2) v c x1
end of h1
(h2)
consider H13
we proved drop (r (Flat f) n0) O x1 e2
drop (S n0) O x1 e2
end of h2
by (H11 . . h1 . h2)
or
drop (S n0) O c e2
ex2 C λe1:C.csubst0 (minus (s (Flat f) x2) (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1
end of H_x
(H14) consider H_x
consider H14
we proved
or
drop (S n0) O c e2
ex2 C λe1:C.csubst0 (minus (s (Flat f) x2) (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1
that is equivalent to or (drop (S n0) O c e2) (ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1)
we proceed by induction on the previous result to prove
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case or_introl : H15:drop (S n0) O c e2 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
consider H15
we proved drop (S n0) O c e2
that is equivalent to drop (r (Flat f) n0) O c e2
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Flat f) t) e2
by (or_introl . . previous)
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case or_intror : H15:ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O c e1 ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
we proceed by induction on H15 to prove
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
case ex_intro2 : x:C H16:csubst0 (minus x2 (S n0)) v x e2 H17:drop (S n0) O c x ⇒
the thesis becomes
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
consider H17
we proved drop (S n0) O c x
that is equivalent to drop (r (Flat f) n0) O c x
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c (Flat f) t) x
by (ex_intro2 . . . . H16 previous)
we proved ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
by (or_intror . . previous)
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
we proved
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
that is equivalent to
or
drop (S n0) O (CHead c (Flat f) t) e2
ex2
C
λe1:C.csubst0 (minus (s (Flat f) x2) (S n0)) v e1 e2
λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
∀H11:∀c3:C
.∀v0:T
.csubst0 (s (Flat f) x2) v0 c c3
→∀e3:C
.drop (S n0) O c3 e3
→(or
drop (S n0) O c e3
ex2 C λe1:C.csubst0 (minus (s (Flat f) x2) (S n0)) v0 e1 e3 λe1:C.drop (S n0) O c e1)
.lt (S n0) (s (Flat f) x2)
→∀H13:drop (r (Flat f) n0) O x1 e2
.or
drop (S n0) O (CHead c (Flat f) t) e2
ex2 C λe1:C.csubst0 (minus x2 (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c (Flat f) t) e1
by (previous . H9 H10 previous)
we proved
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus (s k x2) (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
by (eq_ind_r . . . previous . H4)
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
we proved
or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
∀c2:C
.∀v:T
.∀H1:csubst0 i v (CHead c k t) c2
.∀e2:C
.∀H2:drop (S n0) O c2 e2
.or
drop (S n0) O (CHead c k t) e2
ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O (CHead c k t) e1
we proved
∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop (S n0) O c2 e2
→or (drop (S n0) O c1 e2) (ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O c1 e1)
∀i:nat
.∀H:lt (S n0) i
.∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop (S n0) O c2 e2
→or (drop (S n0) O c1 e2) (ex2 C λe1:C.csubst0 (minus i (S n0)) v e1 e2 λe1:C.drop (S n0) O c1 e1)
we proved
∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop n O c2 e2
→or (drop n O c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.drop n O c1 e1)
we proved
∀n:nat
.∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C
.drop n O c2 e2
→or (drop n O c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.drop n O c1 e1)