DEFINITION pr0_subst0_fwd()
TYPE =
∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst0 i u2 t1 t2)→∀u1:T.(pr0 u2 u1)→(ex2 T λt:T.subst0 i u1 t1 t λt:T.pr0 t2 t)
BODY =
assume u2: T
assume t1: T
assume t2: T
assume i: nat
suppose H: subst0 i u2 t1 t2
we proceed by induction on H to prove ∀u1:T.(pr0 u2 u1)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t2 t4)
case subst0_lref : v:T i0:nat ⇒
the thesis becomes ∀u1:T.∀H0:(pr0 v u1).(ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 (lift (S i0) O v) t)
assume u1: T
suppose H0: pr0 v u1
(h1)
by (subst0_lref . .)
subst0 i0 u1 (TLRef i0) (lift (S i0) O u1)
end of h1
(h2)
by (pr0_lift . . H0 . .)
pr0 (lift (S i0) O v) (lift (S i0) O u1)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 (lift (S i0) O v) t
∀u1:T.∀H0:(pr0 v u1).(ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 (lift (S i0) O v) t)
case subst0_fst : v:T u3:T u1:T i0:nat :subst0 i0 v u1 u3 t:T k:K ⇒
the thesis becomes ∀u0:T.∀H2:(pr0 v u0).(ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0)
(H1) by induction hypothesis we know ∀u4:T.(pr0 v u4)→(ex2 T λt:T.subst0 i0 u4 u1 t λt:T.pr0 u3 t)
assume u0: T
suppose H2: pr0 v u0
by (H1 . H2)
we proved ex2 T λt:T.subst0 i0 u0 u1 t λt:T.pr0 u3 t
we proceed by induction on the previous result to prove ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0
case ex_intro2 : x:T H3:subst0 i0 u0 u1 x H4:pr0 u3 x ⇒
the thesis becomes ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0
(h1)
by (subst0_fst . . . . H3 . .)
subst0 i0 u0 (THead k u1 t) (THead k x t)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (pr0_comp . . H4 . . previous .)
pr0 (THead k u3 t) (THead k x t)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0
we proved ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0
∀u0:T.∀H2:(pr0 v u0).(ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 (THead k u3 t) t0)
case subst0_snd : k:K v:T t3:T t4:T i0:nat :subst0 (s k i0) v t4 t3 u:T ⇒
the thesis becomes ∀u1:T.∀H2:(pr0 v u1).(ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t)
(H1) by induction hypothesis we know ∀u1:T.(pr0 v u1)→(ex2 T λt:T.subst0 (s k i0) u1 t4 t λt:T.pr0 t3 t)
assume u1: T
suppose H2: pr0 v u1
by (H1 . H2)
we proved ex2 T λt:T.subst0 (s k i0) u1 t4 t λt:T.pr0 t3 t
we proceed by induction on the previous result to prove ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t
case ex_intro2 : x:T H3:subst0 (s k i0) u1 t4 x H4:pr0 t3 x ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t
(h1)
by (subst0_snd . . . . . H3 .)
subst0 i0 u1 (THead k u t4) (THead k u x)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 u u
by (pr0_comp . . previous . . H4 .)
pr0 (THead k u t3) (THead k u x)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t
we proved ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t
∀u1:T.∀H2:(pr0 v u1).(ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 (THead k u t3) t)
case subst0_both : v:T u1:T u3:T i0:nat :subst0 i0 v u1 u3 k:K t3:T t4:T :subst0 (s k i0) v t3 t4 ⇒
the thesis becomes ∀u0:T.∀H4:(pr0 v u0).(ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t)
(H1) by induction hypothesis we know ∀u4:T.(pr0 v u4)→(ex2 T λt:T.subst0 i0 u4 u1 t λt:T.pr0 u3 t)
(H3) by induction hypothesis we know ∀u4:T.(pr0 v u4)→(ex2 T λt:T.subst0 (s k i0) u4 t3 t λt:T.pr0 t4 t)
assume u0: T
suppose H4: pr0 v u0
by (H3 . H4)
we proved ex2 T λt:T.subst0 (s k i0) u0 t3 t λt:T.pr0 t4 t
we proceed by induction on the previous result to prove ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
case ex_intro2 : x:T H5:subst0 (s k i0) u0 t3 x H6:pr0 t4 x ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
by (H1 . H4)
we proved ex2 T λt:T.subst0 i0 u0 u1 t λt:T.pr0 u3 t
we proceed by induction on the previous result to prove ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
case ex_intro2 : x0:T H7:subst0 i0 u0 u1 x0 H8:pr0 u3 x0 ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
(h1)
by (subst0_both . . . . H7 . . . H5)
subst0 i0 u0 (THead k u1 t3) (THead k x0 x)
end of h1
(h2)
by (pr0_comp . . H8 . . H6 .)
pr0 (THead k u3 t4) (THead k x0 x)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
we proved ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t
∀u0:T.∀H4:(pr0 v u0).(ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 (THead k u3 t4) t)
we proved ∀u1:T.(pr0 u2 u1)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t2 t4)
we proved ∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst0 i u2 t1 t2)→∀u1:T.(pr0 u2 u1)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t2 t4)