DEFINITION pr0_subst1()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t1 t2)→∀v1:T.∀w1:T.∀i:nat.(subst1 i v1 t1 w1)→∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v2 t2 w2)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pr0 t1 t2
        assume v1: T
        assume w1: T
        assume i: nat
        suppose H0: subst1 i v1 t1 w1
          we proceed by induction on H0 to prove ∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v2 t2 w2)
             case subst1_refl : ⇒
                the thesis becomes ∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 t1 w2 λw2:T.subst1 i v2 t2 w2)
                    assume v2: T
                    suppose : pr0 v1 v2
                      by (subst1_refl . . .)
                      we proved subst1 i v2 t2 t2
                      by (ex_intro2 . . . . H previous)
                      we proved ex2 T λw2:T.pr0 t1 w2 λw2:T.subst1 i v2 t2 w2
∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 t1 w2 λw2:T.subst1 i v2 t2 w2)
             case subst1_single : t0:T H1:subst0 i v1 t1 t0 ⇒
                the thesis becomes ∀v2:T.∀H2:(pr0 v1 v2).(ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2)
                    assume v2: T
                    suppose H2: pr0 v1 v2
                      by (pr0_subst0 . . H . . . H1 . H2)
                      we proved or (pr0 t0 t2) (ex2 T λw2:T.pr0 t0 w2 λw2:T.subst0 i v2 t2 w2)
                      we proceed by induction on the previous result to prove ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                         case or_introl : H3:pr0 t0 t2 ⇒
                            the thesis becomes ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                               by (subst1_refl . . .)
                               we proved subst1 i v2 t2 t2
                               by (ex_intro2 . . . . H3 previous)
ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                         case or_intror : H3:ex2 T λw2:T.pr0 t0 w2 λw2:T.subst0 i v2 t2 w2 ⇒
                            the thesis becomes ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                               we proceed by induction on H3 to prove ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                                  case ex_intro2 : x:T H4:pr0 t0 x H5:subst0 i v2 t2 x ⇒
                                     the thesis becomes ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                                        by (subst1_single . . . . H5)
                                        we proved subst1 i v2 t2 x
                                        by (ex_intro2 . . . . H4 previous)
ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
                      we proved ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2
∀v2:T.∀H2:(pr0 v1 v2).(ex2 T λw2:T.pr0 t0 w2 λw2:T.subst1 i v2 t2 w2)
          we proved ∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v2 t2 w2)
       we proved ∀t1:T.∀t2:T.(pr0 t1 t2)→∀v1:T.∀w1:T.∀i:nat.(subst1 i v1 t1 w1)→∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v2 t2 w2)