DEFINITION pr0_subst0_back()
TYPE =
∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst0 i u2 t1 t2)→∀u1:T.(pr0 u1 u2)→(ex2 T λt:T.subst0 i u1 t1 t λt:T.pr0 t t2)
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 u1 u2)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t4 t2)
case subst0_lref : v:T i0:nat ⇒
the thesis becomes ∀u1:T.∀H0:(pr0 u1 v).(ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 t (lift (S i0) O v))
assume u1: T
suppose H0: pr0 u1 v
(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 u1) (lift (S i0) O v)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 t (lift (S i0) O v)
∀u1:T.∀H0:(pr0 u1 v).(ex2 T λt:T.subst0 i0 u1 (TLRef i0) t λt:T.pr0 t (lift (S i0) O v))
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 u0 v).(ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 t0 (THead k u3 t))
(H1) by induction hypothesis we know ∀u4:T.(pr0 u4 v)→(ex2 T λt:T.subst0 i0 u4 u1 t λt:T.pr0 t u3)
assume u0: T
suppose H2: pr0 u0 v
by (H1 . H2)
we proved ex2 T λt:T.subst0 i0 u0 u1 t λt:T.pr0 t u3
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 t0 (THead k u3 t)
case ex_intro2 : x:T H3:subst0 i0 u0 u1 x H4:pr0 x u3 ⇒
the thesis becomes ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 t0 (THead k u3 t)
(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 x t) (THead k u3 t)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 t0 (THead k u3 t)
we proved ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 t0 (THead k u3 t)
∀u0:T.∀H2:(pr0 u0 v).(ex2 T λt0:T.subst0 i0 u0 (THead k u1 t) t0 λt0:T.pr0 t0 (THead k u3 t))
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 u1 v).(ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 t (THead k u t3))
(H1) by induction hypothesis we know ∀u1:T.(pr0 u1 v)→(ex2 T λt:T.subst0 (s k i0) u1 t4 t λt:T.pr0 t t3)
assume u1: T
suppose H2: pr0 u1 v
by (H1 . H2)
we proved ex2 T λt:T.subst0 (s k i0) u1 t4 t λt:T.pr0 t t3
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 t (THead k u t3)
case ex_intro2 : x:T H3:subst0 (s k i0) u1 t4 x H4:pr0 x t3 ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 t (THead k u t3)
(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 x) (THead k u t3)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 t (THead k u t3)
we proved ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 t (THead k u t3)
∀u1:T.∀H2:(pr0 u1 v).(ex2 T λt:T.subst0 i0 u1 (THead k u t4) t λt:T.pr0 t (THead k u t3))
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 u0 v).(ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4))
(H1) by induction hypothesis we know ∀u4:T.(pr0 u4 v)→(ex2 T λt:T.subst0 i0 u4 u1 t λt:T.pr0 t u3)
(H3) by induction hypothesis we know ∀u4:T.(pr0 u4 v)→(ex2 T λt:T.subst0 (s k i0) u4 t3 t λt:T.pr0 t t4)
assume u0: T
suppose H4: pr0 u0 v
by (H3 . H4)
we proved ex2 T λt:T.subst0 (s k i0) u0 t3 t λt:T.pr0 t t4
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 t (THead k u3 t4)
case ex_intro2 : x:T H5:subst0 (s k i0) u0 t3 x H6:pr0 x t4 ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4)
by (H1 . H4)
we proved ex2 T λt:T.subst0 i0 u0 u1 t λt:T.pr0 t u3
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 t (THead k u3 t4)
case ex_intro2 : x0:T H7:subst0 i0 u0 u1 x0 H8:pr0 x0 u3 ⇒
the thesis becomes ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4)
(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 x0 x) (THead k u3 t4)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4)
ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4)
we proved ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4)
∀u0:T.∀H4:(pr0 u0 v).(ex2 T λt:T.subst0 i0 u0 (THead k u1 t3) t λt:T.pr0 t (THead k u3 t4))
we proved ∀u1:T.(pr0 u1 u2)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t4 t2)
we proved ∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst0 i u2 t1 t2)→∀u1:T.(pr0 u1 u2)→(ex2 T λt4:T.subst0 i u1 t1 t4 λt4:T.pr0 t4 t2)