DEFINITION subst0_lift_lt()
TYPE =
∀t1:T
.∀t2:T
.∀u:T
.∀i:nat
.subst0 i u t1 t2
→∀d:nat
.lt i d
→∀h:nat.(subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
BODY =
assume t1: T
assume t2: T
assume u: T
assume i: nat
suppose H: subst0 i u t1 t2
we proceed by induction on H to prove
∀d:nat
.lt i d
→∀h:nat.(subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
case subst0_lref : v:T i0:nat ⇒
the thesis becomes
∀d:nat
.∀H0:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) v
lift h d (TLRef i0)
lift h d (lift (S i0) O v)
assume d: nat
suppose H0: lt i0 d
assume h: nat
(h1)
(w) by (. . .) we proved
consider H0
we proved lt i0 d
that is equivalent to le (S i0) d
by (le_plus_minus_r . . previous)
we proved eq nat (plus (S i0) (minus d (S i0))) d
we proceed by induction on the previous result to prove subst0 i0 (lift h w v) (TLRef i0) (lift h d (lift (S i0) O v))
case refl_equal : ⇒
the thesis becomes
subst0
i0
lift h w v
TLRef i0
lift h (plus (S i0) (minus d (S i0))) (lift (S i0) O v)
(h1)
by (subst0_lref . .)
we proved
subst0
i0
lift h (minus d (S i0)) v
TLRef i0
lift (S i0) O (lift h (minus d (S i0)) v)
subst0 i0 (lift h w v) (TLRef i0) (lift (S i0) O (lift h (minus d (S i0)) v))
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d (S i0))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S i0) (minus d (S i0))) (lift (S i0) O v)
lift (S i0) O (lift h (minus d (S i0)) v)
end of h2
by (eq_ind_r . . . h1 . h2)
subst0
i0
lift h w v
TLRef i0
lift h (plus (S i0) (minus d (S i0))) (lift (S i0) O v)
we proved
let w := minus d (S i0)
in subst0 i0 (lift h w v) (TLRef i0) (lift h d (lift (S i0) O v))
subst0 i0 (lift h (minus d (S i0)) v) (TLRef i0) (lift h d (lift (S i0) O v))
end of h1
(h2)
by (lift_lref_lt . . . H0)
eq T (lift h d (TLRef i0)) (TLRef i0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
subst0
i0
lift h (minus d (S i0)) v
lift h d (TLRef i0)
lift h d (lift (S i0) O v)
∀d:nat
.∀H0:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) 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:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) v
lift h d (THead k u1 t)
lift h d (THead k u2 t)
(H1) by induction hypothesis we know
∀d:nat
.lt i0 d
→∀h:nat.(subst0 i0 (lift h (minus d (S i0)) v) (lift h d u1) (lift h d u2))
assume d: nat
suppose H2: lt i0 d
assume h: nat
(h1)
(h1)
by (H1 . H2 .)
we proved subst0 i0 (lift h (minus d (S i0)) v) (lift h d u1) (lift h d u2)
by (subst0_fst . . . . previous . .)
subst0
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) v
lift h d (THead k u1 t)
lift h d (THead k u2 t)
∀d:nat
.∀H2:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) 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:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) v
lift h d (THead k u0 t3)
lift h d (THead k u0 t0)
(H1) by induction hypothesis we know
∀d:nat
.lt (s k i0) d
→∀h:nat
.subst0 (s k i0) (lift h (minus d (S (s k i0))) v) (lift h d t3) (lift h d t0)
assume d: nat
suppose H2: lt i0 d
assume h: nat
(H3)
by (s_S . .)
we proved eq nat (s k (S i0)) (S (s k i0))
by (eq_ind_r . . . H1 . previous)
∀d0:nat
.lt (s k i0) d0
→∀h0:nat.(subst0 (s k i0) (lift h0 (minus d0 (s k (S i0))) v) (lift h0 d0 t3) (lift h0 d0 t0))
end of H3
(h1)
(h1)
by (minus_s_s . . .)
we proved eq nat (minus (s k d) (s k (S i0))) (minus d (S i0))
we proceed by induction on the previous result to prove
subst0
i0
lift h (minus d (S i0)) 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)
case refl_equal : ⇒
the thesis becomes
subst0
i0
lift h (minus (s k d) (s k (S i0))) 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)
by (s_lt . . . H2)
we proved lt (s k i0) (s k d)
by (H3 . previous .)
we proved
subst0
s k i0
lift h (minus (s k d) (s k (S i0))) v
lift h (s k d) t3
lift h (s k d) t0
by (subst0_snd . . . . . previous .)
subst0
i0
lift h (minus (s k d) (s k (S i0))) 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)
subst0
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) v
lift h d (THead k u0 t3)
lift h d (THead k u0 t0)
∀d:nat
.∀H2:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) 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:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) v
lift h d (THead k u1 t0)
lift h d (THead k u2 t3)
(H1) by induction hypothesis we know
∀d:nat
.lt i0 d
→∀h:nat.(subst0 i0 (lift h (minus d (S i0)) v) (lift h d u1) (lift h d u2))
(H3) by induction hypothesis we know
∀d:nat
.lt (s k i0) d
→∀h:nat
.subst0 (s k i0) (lift h (minus d (S (s k i0))) v) (lift h d t0) (lift h d t3)
assume d: nat
suppose H4: lt i0 d
assume h: nat
(H5)
by (s_S . .)
we proved eq nat (s k (S i0)) (S (s k i0))
by (eq_ind_r . . . H3 . previous)
∀d0:nat
.lt (s k i0) d0
→∀h0:nat.(subst0 (s k i0) (lift h0 (minus d0 (s k (S i0))) v) (lift h0 d0 t0) (lift h0 d0 t3))
end of H5
(h1)
(h1)
(h1)
by (H1 . H4 .)
subst0 i0 (lift h (minus d (S i0)) v) (lift h d u1) (lift h d u2)
end of h1
(h2)
by (minus_s_s . . .)
we proved eq nat (minus (s k d) (s k (S i0))) (minus d (S i0))
we proceed by induction on the previous result to prove
subst0
s k i0
lift h (minus d (S i0)) v
lift h (s k d) t0
lift h (s k d) t3
case refl_equal : ⇒
the thesis becomes
subst0
s k i0
lift h (minus (s k d) (s k (S i0))) v
lift h (s k d) t0
lift h (s k d) t3
by (s_lt . . . H4)
we proved lt (s k i0) (s k d)
by (H5 . previous .)
subst0
s k i0
lift h (minus (s k d) (s k (S i0))) v
lift h (s k d) t0
lift h (s k d) t3
subst0
s k i0
lift h (minus d (S i0)) v
lift h (s k d) t0
lift h (s k d) t3
end of h2
by (subst0_both . . . . h1 . . . h2)
subst0
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) 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
i0
lift h (minus d (S i0)) v
lift h d (THead k u1 t0)
lift h d (THead k u2 t3)
∀d:nat
.∀H4:lt i0 d
.∀h:nat
.subst0
i0
lift h (minus d (S i0)) v
lift h d (THead k u1 t0)
lift h d (THead k u2 t3)
we proved
∀d:nat
.lt i d
→∀h:nat.(subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
we proved
∀t1:T
.∀t2:T
.∀u:T
.∀i:nat
.subst0 i u t1 t2
→∀d:nat
.lt i d
→∀h:nat.(subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))