DEFINITION pr0_subst1_back()
TYPE =
       ∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst1 i u2 t1 t2)→∀u1:T.(pr0 u1 u2)→(ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t2)
BODY =
        assume u2: T
        assume t1: T
        assume t2: T
        assume i: nat
        suppose H: subst1 i u2 t1 t2
          we proceed by induction on H to prove ∀u1:T.(pr0 u1 u2)→(ex2 T λt0:T.subst1 i u1 t1 t0 λt0:T.pr0 t0 t2)
             case subst1_refl : ⇒
                the thesis becomes ∀u1:T.(pr0 u1 u2)→(ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t1)
                    assume u1: T
                    suppose : pr0 u1 u2
                      (h1) 
                         by (subst1_refl . . .)
subst1 i u1 t1 t1
                      end of h1
                      (h2) by (pr0_refl .) we proved pr0 t1 t1
                      by (ex_intro2 . . . . h1 h2)
                      we proved ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t1
∀u1:T.(pr0 u1 u2)→(ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t1)
             case subst1_single : t0:T H0:subst0 i u2 t1 t0 ⇒
                the thesis becomes ∀u1:T.∀H1:(pr0 u1 u2).(ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0)
                    assume u1: T
                    suppose H1: pr0 u1 u2
                      by (pr0_subst0_back . . . . H0 . H1)
                      we proved ex2 T λt:T.subst0 i u1 t1 t λt:T.pr0 t t0
                      we proceed by induction on the previous result to prove ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0
                         case ex_intro2 : x:T H2:subst0 i u1 t1 x H3:pr0 x t0 ⇒
                            the thesis becomes ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0
                               by (subst1_single . . . . H2)
                               we proved subst1 i u1 t1 x
                               by (ex_intro2 . . . . previous H3)
ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0
                      we proved ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0
∀u1:T.∀H1:(pr0 u1 u2).(ex2 T λt:T.subst1 i u1 t1 t λt:T.pr0 t t0)
          we proved ∀u1:T.(pr0 u1 u2)→(ex2 T λt0:T.subst1 i u1 t1 t0 λt0:T.pr0 t0 t2)
       we proved ∀u2:T.∀t1:T.∀t2:T.∀i:nat.(subst1 i u2 t1 t2)→∀u1:T.(pr0 u1 u2)→(ex2 T λt0:T.subst1 i u1 t1 t0 λt0:T.pr0 t0 t2)