DEFINITION subst0_gen_lift_lt()
TYPE =
∀u:T
.∀t1:T
.∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i (lift h d u) (lift h (S (plus i d)) t1) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i 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 (lift h d u) (lift h (S (plus i d)) t1) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t1 t2
case TSort : n:nat ⇒
the thesis becomes
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i (lift h d u) (lift h (S (plus i d)) (TSort n)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TSort n) t2
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H: subst0 i (lift h d u) (lift h (S (plus i d)) (TSort n)) x
(H0)
by (lift_sort . . .)
we proved eq T (lift h (S (plus i d)) (TSort n)) (TSort n)
we proceed by induction on the previous result to prove subst0 i (lift h d u) (TSort n) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i (lift h d u) (TSort n) x
end of H0
by (subst0_gen_sort . . . . H0 .)
we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TSort n) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i (lift h d u) (lift h (S (plus i d)) (TSort n)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TSort n) t2
case TLRef : n:nat ⇒
the thesis becomes
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i (lift h d u) (lift h (S (plus i d)) (TLRef n)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H: subst0 i (lift h d u) (lift h (S (plus i d)) (TLRef n)) x
(h1)
suppose H0: lt n (S (plus i d))
(H1)
by (lift_lref_lt . . . H0)
we proved eq T (lift h (S (plus i d)) (TLRef n)) (TLRef n)
we proceed by induction on the previous result to prove subst0 i (lift h d u) (TLRef n) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i (lift h d u) (TLRef n) x
end of H1
by (subst0_gen_lref . . . . H1)
we proved land (eq nat n i) (eq T x (lift (S n) O (lift h d u)))
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
case conj : H2:eq nat n i H3:eq T x (lift (S n) O (lift h d u)) ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
by (le_O_n .)
we proved le O d
by (lift_d . . . . . previous)
we proved
eq
T
lift h (plus (S i) d) (lift (S i) O u)
lift (S i) O (lift h d u)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (lift (S i) O (lift h d u)) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (TLRef i) t2
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
lift h (plus (S i) d) (lift (S i) O u)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (TLRef i) t2
(h1)
by (refl_equal . .)
eq
T
lift h (S (plus i d)) (lift (S i) O u)
lift h (S (plus i d)) (lift (S i) O u)
end of h1
(h2)
by (subst0_lref . .)
subst0 i u (TLRef i) (lift (S i) O u)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T
.eq
T
lift h (S (plus i d)) (lift (S i) O u)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (TLRef i) t2
ex2
T
λt2:T
.eq
T
lift h (plus (S i) d) (lift (S i) O u)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (TLRef i) t2
we proved
ex2
T
λt2:T.eq T (lift (S i) O (lift h d u)) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (TLRef i) t2
by (eq_ind_r . . . previous . H2)
we proved
ex2
T
λt2:T.eq T (lift (S n) O (lift h d u)) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (TLRef n) t2
by (eq_ind_r . . . previous . H3)
ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
lt n (S (plus i d))
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
end of h1
(h2)
suppose H0: le (S (plus i d)) n
(H1)
by (lift_lref_ge . . . H0)
we proved eq T (lift h (S (plus i d)) (TLRef n)) (TLRef (plus n h))
we proceed by induction on the previous result to prove subst0 i (lift h d u) (TLRef (plus n h)) x
case refl_equal : ⇒
the thesis becomes the hypothesis H
subst0 i (lift h d u) (TLRef (plus n h)) x
end of H1
by (subst0_gen_lref . . . . H1)
we proved
land
eq nat (plus n h) i
eq T x (lift (S (plus n h)) O (lift h d u))
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
case conj : H2:eq nat (plus n h) i :eq T x (lift (S (plus n h)) O (lift h d u)) ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
(H4)
by (eq_ind_r . . . H0 . H2)
le (S (plus (plus n h) d)) n
end of H4
by (le_plus_l . .)
we proved le n (plus n h)
by (le_plus_trans . . . previous)
we proved le n (plus (plus n h) d)
by (le_false . . . previous H4)
ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
le (S (plus i d)) n
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (TLRef n) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H:subst0 i (lift h d u) (lift h (S (plus i d)) (TLRef n)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i 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 (lift h d u) (lift h (S (plus i d)) (THead k t t0)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
(H) by induction hypothesis we know
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i (lift h d u) (lift h (S (plus i d)) t) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t t2
(H0) by induction hypothesis we know
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i (lift h d u) (lift h (S (plus i d)) t0) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t0 t2
assume x: T
assume i: nat
assume h: nat
assume d: nat
suppose H1: subst0 i (lift h d u) (lift h (S (plus i d)) (THead k t t0)) x
(H2)
by (lift_head . . . . .)
we proved
eq
T
lift h (S (plus i d)) (THead k t t0)
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) t0
we proceed by induction on the previous result to prove
subst0
i
lift h d u
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) t0
x
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0
i
lift h d u
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) t0
x
end of H2
by (subst0_gen_head . . . . . . H2)
we proved
or3
ex2
T
λu2:T.eq T x (THead k u2 (lift h (s k (S (plus i d))) t0))
λu2:T.subst0 i (lift h d u) (lift h (S (plus i d)) t) u2
ex2
T
λt2:T.eq T x (THead k (lift h (S (plus i d)) t) t2)
λt2:T.subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) t2
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead k u2 t2)
λu2:T.λ:T.subst0 i (lift h d u) (lift h (S (plus i d)) t) u2
λ:T.λt2:T.subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) t2
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case or3_intro0 : H3:ex2 T λu2:T.eq T x (THead k u2 (lift h (s k (S (plus i d))) t0)) λu2:T.subst0 i (lift h d u) (lift h (S (plus i d)) t) u2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
we proceed by induction on H3 to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x0:T H4:eq T x (THead k x0 (lift h (s k (S (plus i d))) t0)) H5:subst0 i (lift h d u) (lift h (S (plus i d)) t) x0 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
by (H . . . . H5)
we proved ex2 T λt2:T.eq T x0 (lift h (S (plus i d)) t2) λt2:T.subst0 i 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 (S (plus i d))) t0)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x1:T H6:eq T x0 (lift h (S (plus i d)) x1) H7:subst0 i u t x1 ⇒
the thesis becomes
ex2
T
λt3:T
.eq
T
THead k x0 (lift h (s k (S (plus i d))) t0)
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h (S (plus i d)) (THead k x1 t0)
THead
k
lift h (S (plus i d)) x1
lift h (s k (S (plus i d))) t0
we proceed by induction on the previous result to prove
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) x1
lift h (s k (S (plus i d))) t0
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
lift h (S (plus i d)) (THead k x1 t0)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
(h1)
by (refl_equal . .)
eq
T
lift h (S (plus i d)) (THead k x1 t0)
lift h (S (plus i d)) (THead k x1 t0)
end of h1
(h2)
by (subst0_fst . . . . H7 . .)
subst0 i 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 (S (plus i d)) (THead k x1 t0)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
we proved
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) x1
lift h (s k (S (plus i d))) t0
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (eq_ind_r . . . previous . H6)
ex2
T
λt3:T
.eq
T
THead k x0 (lift h (s k (S (plus i d))) t0)
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
we proved
ex2
T
λt2:T
.eq
T
THead k x0 (lift h (s k (S (plus i d))) t0)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (eq_ind_r . . . previous . H4)
ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case or3_intro1 : H3:ex2 T λt2:T.eq T x (THead k (lift h (S (plus i d)) t) t2) λt2:T.subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) t2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
we proceed by induction on H3 to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x0:T H4:eq T x (THead k (lift h (S (plus i d)) t) x0) H5:subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) x0 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
(H6)
by (s_S . .)
we proved eq nat (s k (S (plus i d))) (S (s k (plus i d)))
we proceed by induction on the previous result to prove subst0 (s k i) (lift h d u) (lift h (S (s k (plus i d))) t0) x0
case refl_equal : ⇒
the thesis becomes the hypothesis H5
subst0 (s k i) (lift h d u) (lift h (S (s k (plus i d))) t0) x0
end of H6
(H7)
by (s_plus . . .)
we proved eq nat (s k (plus i d)) (plus (s k i) d)
we proceed by induction on the previous result to prove subst0 (s k i) (lift h d u) (lift h (S (plus (s k i) d)) t0) x0
case refl_equal : ⇒
the thesis becomes the hypothesis H6
subst0 (s k i) (lift h d u) (lift h (S (plus (s k i) d)) t0) x0
end of H7
by (H0 . . . . H7)
we proved ex2 T λt2:T.eq T x0 (lift h (S (plus (s k i) d)) t2) λt2:T.subst0 (s k i) u t0 t2
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.eq
T
THead k (lift h (S (plus i d)) t) x0
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x1:T H8:eq T x0 (lift h (S (plus (s k i) d)) x1) H9:subst0 (s k i) u t0 x1 ⇒
the thesis becomes
ex2
T
λt3:T
.eq
T
THead k (lift h (S (plus i d)) t) x0
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (s_plus . . .)
we proved eq nat (s k (plus i d)) (plus (s k i) d)
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (S (plus (s k i) d)) x1
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (S (s k (plus i d))) x1
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (s_S . .)
we proved eq nat (s k (S (plus i d))) (S (s k (plus i d)))
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (S (s k (plus i d))) x1
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case refl_equal : ⇒
the thesis becomes
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) x1
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h (S (plus i d)) (THead k t x1)
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) x1
we proceed by induction on the previous result to prove
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) x1
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
lift h (S (plus i d)) (THead k t x1)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
(h1)
by (refl_equal . .)
eq
T
lift h (S (plus i d)) (THead k t x1)
lift h (S (plus i d)) (THead k t x1)
end of h1
(h2)
by (subst0_snd . . . . . H9 .)
subst0 i 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 (S (plus i d)) (THead k t x1)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (s k (S (plus i d))) x1
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (S (s k (plus i d))) x1
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
we proved
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) t
lift h (S (plus (s k i) d)) x1
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (eq_ind_r . . . previous . H8)
ex2
T
λt3:T
.eq
T
THead k (lift h (S (plus i d)) t) x0
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
we proved
ex2
T
λt2:T
.eq
T
THead k (lift h (S (plus i d)) t) x0
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (eq_ind_r . . . previous . H4)
ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case or3_intro2 : H3:ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i (lift h d u) (lift h (S (plus i d)) t) u2 λ:T.λt2:T.subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) t2 ⇒
the thesis becomes ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
we proceed by induction on H3 to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
case ex3_2_intro : x0:T x1:T H4:eq T x (THead k x0 x1) H5:subst0 i (lift h d u) (lift h (S (plus i d)) t) x0 H6:subst0 (s k i) (lift h d u) (lift h (s k (S (plus i d))) t0) x1 ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
(H7)
by (s_S . .)
we proved eq nat (s k (S (plus i d))) (S (s k (plus i d)))
we proceed by induction on the previous result to prove subst0 (s k i) (lift h d u) (lift h (S (s k (plus i d))) t0) x1
case refl_equal : ⇒
the thesis becomes the hypothesis H6
subst0 (s k i) (lift h d u) (lift h (S (s k (plus i d))) t0) x1
end of H7
(H8)
by (s_plus . . .)
we proved eq nat (s k (plus i d)) (plus (s k i) d)
we proceed by induction on the previous result to prove subst0 (s k i) (lift h d u) (lift h (S (plus (s k i) d)) t0) x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
subst0 (s k i) (lift h d u) (lift h (S (plus (s k i) d)) t0) x1
end of H8
by (H0 . . . . H8)
we proved ex2 T λt2:T.eq T x1 (lift h (S (plus (s k i) d)) t2) λt2:T.subst0 (s k i) 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 (S (plus i d)) t2)
λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x2:T H9:eq T x1 (lift h (S (plus (s k i) d)) x2) H10:subst0 (s k i) u t0 x2 ⇒
the thesis becomes
ex2
T
λt2:T.eq T (THead k x0 x1) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (THead k t t0) t2
by (H . . . . H5)
we proved ex2 T λt2:T.eq T x0 (lift h (S (plus i d)) t2) λt2:T.subst0 i 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 (S (plus i d)) t2)
λt2:T.subst0 i u (THead k t t0) t2
case ex_intro2 : x3:T H11:eq T x0 (lift h (S (plus i d)) x3) H12:subst0 i u t x3 ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead k x0 x1) (lift h (S (plus i d)) t3)
λt3:T.subst0 i u (THead k t t0) t3
by (s_plus . . .)
we proved eq nat (s k (plus i d)) (plus (s k i) d)
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (S (plus (s k i) d)) x2
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (S (s k (plus i d))) x2
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (s_S . .)
we proved eq nat (s k (S (plus i d))) (S (s k (plus i d)))
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (S (s k (plus i d))) x2
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
case refl_equal : ⇒
the thesis becomes
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (s k (S (plus i d))) x2
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (lift_head . . . . .)
we proved
eq
T
lift h (S (plus i d)) (THead k x3 x2)
THead
k
lift h (S (plus i d)) x3
lift h (s k (S (plus i d))) x2
we proceed by induction on the previous result to prove
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (s k (S (plus i d))) x2
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
case refl_equal : ⇒
the thesis becomes
ex2
T
λt2:T
.eq
T
lift h (S (plus i d)) (THead k x3 x2)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
(h1)
by (refl_equal . .)
eq
T
lift h (S (plus i d)) (THead k x3 x2)
lift h (S (plus i d)) (THead k x3 x2)
end of h1
(h2)
by (subst0_both . . . . H12 . . . H10)
subst0 i 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 (S (plus i d)) (THead k x3 x2)
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
ex2
T
λt3:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (s k (S (plus i d))) x2
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (S (s k (plus i d))) x2
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
we proved
ex2
T
λt2:T
.eq
T
THead
k
lift h (S (plus i d)) x3
lift h (S (plus (s k i) d)) x2
lift h (S (plus i d)) t2
λt2:T.subst0 i u (THead k t t0) t2
by (eq_ind_r . . . previous . H9)
we proved
ex2
T
λt3:T
.eq
T
THead k (lift h (S (plus i d)) x3) x1
lift h (S (plus i d)) t3
λt3:T.subst0 i u (THead k t t0) t3
by (eq_ind_r . . . previous . H11)
ex2
T
λt3:T.eq T (THead k x0 x1) (lift h (S (plus i d)) t3)
λt3:T.subst0 i u (THead k t t0) t3
ex2
T
λt2:T.eq T (THead k x0 x1) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (THead k t t0) t2
we proved
ex2
T
λt2:T.eq T (THead k x0 x1) (lift h (S (plus i d)) t2)
λt2:T.subst0 i u (THead k t t0) t2
by (eq_ind_r . . . previous . H4)
ex2 T λt3:T.eq T x (lift h (S (plus i d)) t3) λt3:T.subst0 i u (THead k t t0) t3
ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.∀H1:subst0 i (lift h d u) (lift h (S (plus i d)) (THead k t t0)) x
.ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u (THead k t t0) t2
we proved
∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i (lift h d u) (lift h (S (plus i d)) t1) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t1 t2
we proved
∀u:T
.∀t1:T
.∀x:T
.∀i:nat
.∀h:nat
.∀d:nat
.subst0 i (lift h d u) (lift h (S (plus i d)) t1) x
→ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t1 t2