DEFINITION subst0_lift_ge()
TYPE =
∀t1:T
.∀t2:T
.∀u:T
.∀i:nat
.∀h:nat
.subst0 i u t1 t2
→∀d:nat.(le d i)→(subst0 (plus i h) u (lift h d t1) (lift h d t2))
BODY =
assume t1: T
assume t2: T
assume u: T
assume i: nat
assume h: nat
suppose H: subst0 i u t1 t2
we proceed by induction on H to prove ∀d:nat.(le d i)→(subst0 (plus i h) u (lift h d t1) (lift h d t2))
case subst0_lref : v:T i0:nat ⇒
the thesis becomes
∀d:nat
.∀H0:le d i0
.subst0 (plus i0 h) v (lift h d (TLRef i0)) (lift h d (lift (S i0) O v))
assume d: nat
suppose H0: le d i0
(h1)
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus h i0)) (plus h (S i0))
we proceed by induction on the previous result to prove subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift (plus h (S i0)) O v)
case refl_equal : ⇒
the thesis becomes subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift (S (plus h i0)) O v)
(h1)
by (subst0_lref . .)
subst0 (plus h i0) v (TLRef (plus h i0)) (lift (S (plus h i0)) O v)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i0 h) (plus h i0)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift (S (plus h i0)) O v)
subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift (plus h (S i0)) O v)
end of h1
(h2)
(h1)
by (le_S . . H0)
we proved le d (S i0)
le d (plus O (S i0))
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 i0) O v)) (lift (plus h (S i0)) O v)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift h d (lift (S i0) O v))
end of h1
(h2)
by (lift_lref_ge . . . H0)
eq T (lift h d (TLRef i0)) (TLRef (plus i0 h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 (plus i0 h) v (lift h d (TLRef i0)) (lift h d (lift (S i0) O v))
∀d:nat
.∀H0:le d i0
.subst0 (plus i0 h) v (lift h d (TLRef i0)) (lift h d (lift (S i0) O v))
case subst0_fst : v:T u2:T u1:T i0:nat :subst0 i0 v u1 u2 t:T k:K ⇒
the thesis becomes
∀d:nat
.∀H2:le d i0
.subst0 (plus i0 h) v (lift h d (THead k u1 t)) (lift h d (THead k u2 t))
(H1) by induction hypothesis we know ∀d:nat.(le d i0)→(subst0 (plus i0 h) v (lift h d u1) (lift h d u2))
assume d: nat
suppose H2: le d i0
(h1)
(h1)
by (H1 . H2)
we proved subst0 (plus i0 h) v (lift h d u1) (lift h d u2)
by (subst0_fst . . . . previous . .)
subst0
plus i0 h
v
THead k (lift h d u1) (lift h (s k d) t)
THead k (lift h d u2) (lift h (s k d) t)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u2 t)
THead k (lift h d u2) (lift h (s k d) t)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0
plus i0 h
v
THead k (lift h d u1) (lift h (s k d) t)
lift h d (THead k u2 t)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u1 t)
THead k (lift h d u1) (lift h (s k d) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 (plus i0 h) v (lift h d (THead k u1 t)) (lift h d (THead k u2 t))
∀d:nat
.∀H2:le d i0
.subst0 (plus i0 h) v (lift h d (THead k u1 t)) (lift h d (THead k u2 t))
case subst0_snd : k:K v:T t0:T t3:T i0:nat :subst0 (s k i0) v t3 t0 u0:T ⇒
the thesis becomes
∀d:nat
.∀H2:(le d i0).(subst0 (plus i0 h) v (lift h d (THead k u0 t3)) (lift h d (THead k u0 t0)))
(H1) by induction hypothesis we know
∀d:nat.(le d (s k i0))→(subst0 (plus (s k i0) h) v (lift h d t3) (lift h d t0))
assume d: nat
suppose H2: le d i0
(H3)
by (s_plus . . .)
we proved eq nat (s k (plus i0 h)) (plus (s k i0) h)
by (eq_ind_r . . . H1 . previous)
∀d0:nat.(le d0 (s k i0))→(subst0 (s k (plus i0 h)) v (lift h d0 t3) (lift h d0 t0))
end of H3
(h1)
(h1)
by (s_le . . . H2)
we proved le (s k d) (s k i0)
by (H3 . previous)
we proved subst0 (s k (plus i0 h)) v (lift h (s k d) t3) (lift h (s k d) t0)
by (subst0_snd . . . . . previous .)
subst0
plus i0 h
v
THead k (lift h d u0) (lift h (s k d) t3)
THead k (lift h d u0) (lift h (s k d) t0)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u0 t0)
THead k (lift h d u0) (lift h (s k d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0
plus i0 h
v
THead k (lift h d u0) (lift h (s k d) t3)
lift h d (THead k u0 t0)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u0 t3)
THead k (lift h d u0) (lift h (s k d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 (plus i0 h) v (lift h d (THead k u0 t3)) (lift h d (THead k u0 t0))
∀d:nat
.∀H2:(le d i0).(subst0 (plus i0 h) v (lift h d (THead k u0 t3)) (lift h d (THead k u0 t0)))
case subst0_both : v:T u1:T u2:T i0:nat :subst0 i0 v u1 u2 k:K t0:T t3:T :subst0 (s k i0) v t0 t3 ⇒
the thesis becomes
∀d:nat
.∀H4:(le d i0).(subst0 (plus i0 h) v (lift h d (THead k u1 t0)) (lift h d (THead k u2 t3)))
(H1) by induction hypothesis we know ∀d:nat.(le d i0)→(subst0 (plus i0 h) v (lift h d u1) (lift h d u2))
(H3) by induction hypothesis we know
∀d:nat.(le d (s k i0))→(subst0 (plus (s k i0) h) v (lift h d t0) (lift h d t3))
assume d: nat
suppose H4: le d i0
(H5)
by (s_plus . . .)
we proved eq nat (s k (plus i0 h)) (plus (s k i0) h)
by (eq_ind_r . . . H3 . previous)
∀d0:nat.(le d0 (s k i0))→(subst0 (s k (plus i0 h)) v (lift h d0 t0) (lift h d0 t3))
end of H5
(h1)
(h1)
(h1)
by (H1 . H4)
subst0 (plus i0 h) v (lift h d u1) (lift h d u2)
end of h1
(h2)
by (s_le . . . H4)
we proved le (s k d) (s k i0)
by (H5 . previous)
subst0 (s k (plus i0 h)) v (lift h (s k d) t0) (lift h (s k d) t3)
end of h2
by (subst0_both . . . . h1 . . . h2)
subst0
plus i0 h
v
THead k (lift h d u1) (lift h (s k d) t0)
THead k (lift h d u2) (lift h (s k d) t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u2 t3)
THead k (lift h d u2) (lift h (s k d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0
plus i0 h
v
THead k (lift h d u1) (lift h (s k d) t0)
lift h d (THead k u2 t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k u1 t0)
THead k (lift h d u1) (lift h (s k d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 (plus i0 h) v (lift h d (THead k u1 t0)) (lift h d (THead k u2 t3))
∀d:nat
.∀H4:(le d i0).(subst0 (plus i0 h) v (lift h d (THead k u1 t0)) (lift h d (THead k u2 t3)))
we proved ∀d:nat.(le d i)→(subst0 (plus i h) u (lift h d t1) (lift h d t2))
we proved
∀t1:T
.∀t2:T
.∀u:T
.∀i:nat
.∀h:nat
.subst0 i u t1 t2
→∀d:nat.(le d i)→(subst0 (plus i h) u (lift h d t1) (lift h d t2))