DEFINITION subst0_gen_lift_false()
TYPE =
∀t:T
.∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t) x)→∀P:Prop.P
BODY =
assume t: T
we proceed by induction on t to prove
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t) x)→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→∀H1:(subst0 i u (lift h d (TSort n)) x).∀P:Prop.P
assume u: T
assume x: T
assume h: nat
assume d: nat
assume i: nat
suppose : le d i
suppose : lt i (plus d h)
suppose H1: subst0 i u (lift h d (TSort n)) x
assume P: Prop
(H2)
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 H1
subst0 i u (TSort n) x
end of H2
by (subst0_gen_sort . . . . H2 .)
we proved P
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→∀H1:(subst0 i u (lift h d (TSort n)) x).∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.∀H:(le d i).∀H0:(lt i (plus d h)).∀H1:(subst0 i u (lift h d (TLRef n)) x).∀P:Prop.P
assume u: T
assume x: T
assume h: nat
assume d: nat
assume i: nat
suppose H: le d i
suppose H0: lt i (plus d h)
suppose H1: subst0 i u (lift h d (TLRef n)) x
assume P: Prop
(h1)
suppose H2: lt n d
(H3)
by (lift_lref_lt . . . H2)
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 H1
subst0 i u (TLRef n) x
end of H3
by (subst0_gen_lref . . . . H3)
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 P
case conj : H4:eq nat n i :eq T x (lift (S n) O u) ⇒
the thesis becomes P
(H6)
we proceed by induction on H4 to prove lt i d
case refl_equal : ⇒
the thesis becomes the hypothesis H2
lt i d
end of H6
consider H6
we proved lt i d
that is equivalent to le (S i) d
by (le_false . . . H previous)
P
we proved P
(lt n d)→P
end of h1
(h2)
suppose H2: le d n
(H3)
by (lift_lref_ge . . . H2)
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 H1
subst0 i u (TLRef (plus n h)) x
end of H3
by (subst0_gen_lref . . . . H3)
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 P
case conj : H4:eq nat (plus n h) i :eq T x (lift (S (plus n h)) O u) ⇒
the thesis becomes P
(H6)
by (eq_ind_r . . . H0 . H4)
lt (plus n h) (plus d h)
end of H6
by (simpl_lt_plus_r . . . H6)
we proved lt n d
by (lt_le_S . . previous)
we proved le (S n) d
by (le_false . . . H2 previous)
P
we proved P
(le d n)→P
end of h2
by (lt_le_e . . . h1 h2)
we proved P
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.∀H:(le d i).∀H0:(lt i (plus d h)).∀H1:(subst0 i u (lift h d (TLRef n)) x).∀P:Prop.P
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.∀H1:(le d i).∀H2:(lt i (plus d h)).∀H3:(subst0 i u (lift h d (THead k t0 t1)) x).∀P:Prop.P
(H) by induction hypothesis we know
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t0) x)→∀P:Prop.P
(H0) by induction hypothesis we know
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t1) x)→∀P:Prop.P
assume u: T
assume x: T
assume h: nat
assume d: nat
assume i: nat
suppose H1: le d i
suppose H2: lt i (plus d h)
suppose H3: subst0 i u (lift h d (THead k t0 t1)) x
assume P: Prop
(H4)
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k t0 t1)
THead k (lift h d t0) (lift h (s k d) t1)
we proceed by induction on the previous result to prove subst0 i u (THead k (lift h d t0) (lift h (s k d) t1)) x
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead k (lift h d t0) (lift h (s k d) t1)) x
end of H4
by (subst0_gen_head . . . . . . H4)
we proved
or3
ex2 T λu2:T.eq T x (THead k u2 (lift h (s k d) t1)) λu2:T.subst0 i u (lift h d t0) u2
ex2 T λt2:T.eq T x (THead k (lift h d t0) t2) λt2:T.subst0 (s k i) u (lift h (s k d) t1) 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 t0) u2
λ:T.λt2:T.subst0 (s k i) u (lift h (s k d) t1) t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H5:ex2 T λu2:T.eq T x (THead k u2 (lift h (s k d) t1)) λu2:T.subst0 i u (lift h d t0) u2 ⇒
the thesis becomes P
we proceed by induction on H5 to prove P
case ex_intro2 : x0:T :eq T x (THead k x0 (lift h (s k d) t1)) H7:subst0 i u (lift h d t0) x0 ⇒
the thesis becomes P
by (H . . . . . H1 H2 H7 .)
P
P
case or3_intro1 : H5:ex2 T λt2:T.eq T x (THead k (lift h d t0) t2) λt2:T.subst0 (s k i) u (lift h (s k d) t1) t2 ⇒
the thesis becomes P
we proceed by induction on H5 to prove P
case ex_intro2 : x0:T :eq T x (THead k (lift h d t0) x0) H7:subst0 (s k i) u (lift h (s k d) t1) x0 ⇒
the thesis becomes P
(h1)
by (s_le . . . H1)
le (s k d) (s k i)
end of h1
(h2)
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 lt (s k i) (plus (s k d) h)
case refl_equal : ⇒
the thesis becomes lt (s k i) (s k (plus d h))
by (s_lt . . . H2)
we proved lt (s k i) (s k (plus d h))
by (lt_le_S . . previous)
we proved le (S (s k i)) (s k (plus d h))
lt (s k i) (s k (plus d h))
lt (s k i) (plus (s k d) h)
end of h2
by (H0 . . . . . h1 h2 H7 .)
P
P
case or3_intro2 : H5:ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i u (lift h d t0) u2 λ:T.λt2:T.subst0 (s k i) u (lift h (s k d) t1) t2 ⇒
the thesis becomes P
we proceed by induction on H5 to prove P
case ex3_2_intro : x0:T x1:T :eq T x (THead k x0 x1) H7:subst0 i u (lift h d t0) x0 :subst0 (s k i) u (lift h (s k d) t1) x1 ⇒
the thesis becomes P
by (H . . . . . H1 H2 H7 .)
P
P
we proved P
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.∀H1:(le d i).∀H2:(lt i (plus d h)).∀H3:(subst0 i u (lift h d (THead k t0 t1)) x).∀P:Prop.P
we proved
∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t) x)→∀P:Prop.P
we proved
∀t:T
.∀u:T
.∀x:T
.∀h:nat
.∀d:nat
.∀i:nat
.le d i
→(lt i (plus d h))→(subst0 i u (lift h d t) x)→∀P:Prop.P