DEFINITION subst0_gen_lift_ge()
TYPE =
∀u:T
.∀t1:T
.∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t1) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t1 t2)
BODY =
assume u: T
assume t1: T
we proceed by induction on t1 to prove
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t1) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t1 t2)
case TSort : n:nat ⇒
the thesis becomes
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i u (lift h d (TSort n)) x
.le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TSort n) t2
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H: subst0 i u (lift h d (TSort n)) x
suppose : le (plus d h) i
(H1)
by (lift_sort . . .)
we proved eq T (lift h d (TSort n)) (TSort n)
we proceed by induction on the previous result to prove subst0 i u (TSort n) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i u (TSort n) x
end of H1
by (subst0_gen_sort . . . . H1 .)
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TSort n) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i u (lift h d (TSort n)) x
.le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TSort n) t2
case TLRef : n:nat ⇒
the thesis becomes
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i u (lift h d (TLRef n)) x
.∀H0:le (plus d h) i
.ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H: subst0 i u (lift h d (TLRef n)) x
suppose H0: le (plus d h) i
(h1)
suppose H1: lt n d
(H2)
by (lift_lref_lt . . . H1)
we proved eq T (lift h d (TLRef n)) (TLRef n)
we proceed by induction on the previous result to prove subst0 i u (TLRef n) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i u (TLRef n) x
end of H2
by (subst0_gen_lref . . . . H2)
we proved land (eq nat n i) (eq T x (lift (S n) O u))
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
case conj : H3:eq nat n i :eq T x (lift (S n) O u) ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
(H5)
we proceed by induction on H3 to prove lt i d
case refl_equal : ⇒
the thesis becomes the hypothesis H1
lt i d
end of H5
consider H5
we proved lt i d
that is equivalent to le (S i) d
by (le_plus_trans . . . previous)
we proved le (S i) (plus d h)
by (le_false . . . H0 previous)
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
lt n d
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
end of h1
(h2)
suppose H1: le d n
(H2)
by (lift_lref_ge . . . H1)
we proved eq T (lift h d (TLRef n)) (TLRef (plus n h))
we proceed by induction on the previous result to prove subst0 i u (TLRef (plus n h)) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i u (TLRef (plus n h)) x
end of H2
by (subst0_gen_lref . . . . H2)
we proved land (eq nat (plus n h) i) (eq T x (lift (S (plus n h)) O u))
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
case conj : H3:eq nat (plus n h) i H4:eq T x (lift (S (plus n h)) O u) ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
we proceed by induction on H3 to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
case refl_equal : ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus (plus n h) h) u (TLRef n) t2
(h1)
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (lift (plus h (S n)) O u) (lift (plus h (S n)) O u)
end of h1
(h2)
by (plus_n_Sm . .)
eq nat (S (plus h n)) (plus h (S n))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (lift (S (plus h n)) O u) (lift (plus h (S n)) O u)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus n h) (plus h n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (lift (S (plus n h)) O u) (lift (plus h (S n)) O u)
end of h1
(h2)
(h1)
(h1) by (le_n .) we proved le O O
(h2)
by (le_S . . H1)
le d (S n)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved le (plus O d) (plus O (S n))
by (le_trans_plus_r . . . previous)
le d (plus O (S n))
end of h1
(h2) by (le_O_n .) we proved le O d
by (lift_free . . . . . h1 h2)
eq T (lift h d (lift (S n) O u)) (lift (plus h (S n)) O u)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (lift (S (plus n h)) O u) (lift h d (lift (S n) O u))
end of h1
(h2)
by (subst0_lref . .)
subst0 n u (TLRef n) (lift (S n) O u)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (lift (S (plus n h)) O u) (lift h d t2)
λt2:T.subst0 n u (TLRef n) t2
end of h1
(h2)
by (minus_plus_r . .)
eq nat (minus (plus n h) h) n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex2
T
λt2:T.eq T (lift (S (plus n h)) O u) (lift h d t2)
λt2:T.subst0 (minus (plus n h) h) u (TLRef n) t2
by (eq_ind_r . . . previous . H4)
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus (plus n h) h) u (TLRef n) t2
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
le d n
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i u (lift h d (TLRef n)) x
.∀H0:le (plus d h) i
.ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (TLRef n) t2
case THead : k:K t:T t0:T ⇒
the thesis becomes
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H1:subst0 i u (lift h d (THead k t t0)) x
.∀H2:le (plus d h) i
.ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
(H) by induction hypothesis we know
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t t2)
(H0) by induction hypothesis we know
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t0) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t0 t2)
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H1: subst0 i u (lift h d (THead k t t0)) x
suppose H2: le (plus d h) i
(H3)
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k t t0)
THead k (lift h d t) (lift h (s k d) t0)
we proceed by induction on the previous result to prove subst0 i u (THead k (lift h d t) (lift h (s k d) t0)) x
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i u (THead k (lift h d t) (lift h (s k d) t0)) x
end of H3
by (subst0_gen_head . . . . . . H3)
we proved
or3
ex2 T λu2:T.eq T x (THead k u2 (lift h (s k d) t0)) λu2:T.subst0 i u (lift h d t) u2
ex2
T
λt2:T.eq T x (THead k (lift h d t) t2)
λt2:T.subst0 (s k i) u (lift h (s k d) t0) t2
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead k u2 t2)
λu2:T.λ:T.subst0 i u (lift h d t) u2
λ:T.λt2:T.subst0 (s k i) u (lift h (s k d) t0) t2
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case or3_intro0 : H4:ex2 T λu2:T.eq T x (THead k u2 (lift h (s k d) t0)) λu2:T.subst0 i u (lift h d t) u2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proceed by induction on H4 to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x0:T H5:eq T x (THead k x0 (lift h (s k d) t0)) H6:subst0 i u (lift h d t) x0 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (H . . . . H6 H2)
we proved ex2 T λt2:T.eq T x0 (lift h d t2) λt2:T.subst0 (minus i h) u t t2
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead k x0 (lift h (s k d) t0)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x1:T H7:eq T x0 (lift h d x1) H8:subst0 (minus i h) u t x1 ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead k x0 (lift h (s k d) t0)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k x1 t0)
THead k (lift h d x1) (lift h (s k d) t0)
we proceed by induction on the previous result to prove
ex2
T
λt3:T.eq T (THead k (lift h d x1) (lift h (s k d) t0)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T.eq T (lift h d (THead k x1 t0)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
(h1)
by (refl_equal . .)
eq T (lift h d (THead k x1 t0)) (lift h d (THead k x1 t0))
end of h1
(h2)
by (subst0_fst . . . . H8 . .)
subst0 (minus i h) u (THead k t t0) (THead k x1 t0)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (lift h d (THead k x1 t0)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved
ex2
T
λt3:T.eq T (THead k (lift h d x1) (lift h (s k d) t0)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (eq_ind_r . . . previous . H7)
ex2
T
λt3:T.eq T (THead k x0 (lift h (s k d) t0)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
we proved
ex2
T
λt2:T.eq T (THead k x0 (lift h (s k d) t0)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case or3_intro1 : H4:ex2 T λt2:T.eq T x (THead k (lift h d t) t2) λt2:T.subst0 (s k i) u (lift h (s k d) t0) t2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proceed by induction on H4 to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x0:T H5:eq T x (THead k (lift h d t) x0) H6:subst0 (s k i) u (lift h (s k d) t0) x0 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (s_plus . . .)
we proved eq nat (s k (plus d h)) (plus (s k d) h)
we proceed by induction on the previous result to prove le (plus (s k d) h) (s k i)
case refl_equal : ⇒
the thesis becomes le (s k (plus d h)) (s k i)
by (s_le . . . H2)
le (s k (plus d h)) (s k i)
we proved le (plus (s k d) h) (s k i)
by (H0 . . . . H6 previous)
we proved ex2 T λt2:T.eq T x0 (lift h (s k d) t2) λt2:T.subst0 (minus (s k i) h) u t0 t2
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead k (lift h d t) x0) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x1:T H7:eq T x0 (lift h (s k d) x1) H8:subst0 (minus (s k i) h) u t0 x1 ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead k (lift h d t) x0) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k t x1)
THead k (lift h d t) (lift h (s k d) x1)
we proceed by induction on the previous result to prove
ex2
T
λt3:T.eq T (THead k (lift h d t) (lift h (s k d) x1)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T.eq T (lift h d (THead k t x1)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
(H9)
by (le_trans_plus_r . . . H2)
we proved le h i
by (s_minus . . . previous)
we proved eq nat (s k (minus i h)) (minus (s k i) h)
by (eq_ind_r . . . H8 . previous)
subst0 (s k (minus i h)) u t0 x1
end of H9
(h1)
by (refl_equal . .)
eq T (lift h d (THead k t x1)) (lift h d (THead k t x1))
end of h1
(h2)
by (subst0_snd . . . . . H9 .)
subst0 (minus i h) u (THead k t t0) (THead k t x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (lift h d (THead k t x1)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved
ex2
T
λt3:T.eq T (THead k (lift h d t) (lift h (s k d) x1)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (eq_ind_r . . . previous . H7)
ex2
T
λt3:T.eq T (THead k (lift h d t) x0) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
we proved
ex2
T
λt2:T.eq T (THead k (lift h d t) x0) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case or3_intro2 : H4:ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i u (lift h d t) u2 λ:T.λt2:T.subst0 (s k i) u (lift h (s k d) t0) t2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proceed by induction on H4 to prove ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex3_2_intro : x0:T x1:T H5:eq T x (THead k x0 x1) H6:subst0 i u (lift h d t) x0 H7:subst0 (s k i) u (lift h (s k d) t0) x1 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (s_plus . . .)
we proved eq nat (s k (plus d h)) (plus (s k d) h)
we proceed by induction on the previous result to prove le (plus (s k d) h) (s k i)
case refl_equal : ⇒
the thesis becomes le (s k (plus d h)) (s k i)
by (s_le . . . H2)
le (s k (plus d h)) (s k i)
we proved le (plus (s k d) h) (s k i)
by (H0 . . . . H7 previous)
we proved ex2 T λt2:T.eq T x1 (lift h (s k d) t2) λt2:T.subst0 (minus (s k i) h) u t0 t2
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T (THead k x0 x1) (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x2:T H8:eq T x1 (lift h (s k d) x2) H9:subst0 (minus (s k i) h) u t0 x2 ⇒
the thesis becomes ex2 T λt2:T.eq T (THead k x0 x1) (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
by (H . . . . H6 H2)
we proved ex2 T λt2:T.eq T x0 (lift h d t2) λt2:T.subst0 (minus i h) u t t2
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T (THead k x0 x1) (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
case ex_intro2 : x3:T H10:eq T x0 (lift h d x3) H11:subst0 (minus i h) u t x3 ⇒
the thesis becomes ex2 T λt3:T.eq T (THead k x0 x1) (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k x3 x2)
THead k (lift h d x3) (lift h (s k d) x2)
we proceed by induction on the previous result to prove
ex2
T
λt3:T.eq T (THead k (lift h d x3) (lift h (s k d) x2)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T.eq T (lift h d (THead k x3 x2)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
(H12)
by (le_trans_plus_r . . . H2)
we proved le h i
by (s_minus . . . previous)
we proved eq nat (s k (minus i h)) (minus (s k i) h)
by (eq_ind_r . . . H9 . previous)
subst0 (s k (minus i h)) u t0 x2
end of H12
(h1)
by (refl_equal . .)
eq T (lift h d (THead k x3 x2)) (lift h d (THead k x3 x2))
end of h1
(h2)
by (subst0_both . . . . H11 . . . H12)
subst0 (minus i h) u (THead k t t0) (THead k x3 x2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (lift h d (THead k x3 x2)) (lift h d t2)
λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved
ex2
T
λt3:T.eq T (THead k (lift h d x3) (lift h (s k d) x2)) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (eq_ind_r . . . previous . H8)
we proved
ex2
T
λt3:T.eq T (THead k (lift h d x3) x1) (lift h d t3)
λt3:T.subst0 (minus i h) u (THead k t t0) t3
by (eq_ind_r . . . previous . H10)
ex2 T λt3:T.eq T (THead k x0 x1) (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
ex2 T λt2:T.eq T (THead k x0 x1) (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved ex2 T λt2:T.eq T (THead k x0 x1) (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T x (lift h d t3) λt3:T.subst0 (minus i h) u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H1:subst0 i u (lift h d (THead k t t0)) x
.∀H2:le (plus d h) i
.ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u (THead k t t0) t2
we proved
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t1) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t1 t2)
we proved
∀u:T
.∀t1:T
.∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i u (lift h d t1) x
→(le (plus d h) i
→ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst0 (minus i h) u t1 t2)