DEFINITION pr0_confluence__pr0_upsilon_upsilon()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀v1:T
                .∀v2:T
                  .∀x0:T
                    .pr0 v1 x0
                      →(pr0 v2 x0
                           →∀u1:T
                                .∀u2:T
                                  .∀x1:T
                                    .pr0 u1 x1
                                      →(pr0 u2 x1
                                           →∀t1:T
                                                .∀t2:T
                                                  .∀x2:T
                                                    .pr0 t1 x2
                                                      →(pr0 t2 x2
                                                           →(ex2
                                                                T
                                                                λt:T.pr0 (THead (Bind b) u1 (THead (Flat Appl) (lift (S O) O v1) t1)) t
                                                                λt:T.pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) t))))
BODY =
        assume b: B
        suppose : not (eq B b Abst)
        assume v1: T
        assume v2: T
        assume x0: T
        suppose H0: pr0 v1 x0
        suppose H1: pr0 v2 x0
        assume u1: T
        assume u2: T
        assume x1: T
        suppose H2: pr0 u1 x1
        suppose H3: pr0 u2 x1
        assume t1: T
        assume t2: T
        assume x2: T
        suppose H4: pr0 t1 x2
        suppose H5: pr0 t2 x2
          (h1) 
             by (pr0_lift . . H0 . .)
             we proved pr0 (lift (S O) O v1) (lift (S O) O x0)
             by (pr0_comp . . previous . . H4 .)
             we proved 
                pr0
                  THead (Flat Appl) (lift (S O) O v1) t1
                  THead (Flat Appl) (lift (S O) O x0) x2
             by (pr0_comp . . H2 . . previous .)

                pr0
                  THead (Bind b) u1 (THead (Flat Appl) (lift (S O) O v1) t1)
                  THead (Bind b) x1 (THead (Flat Appl) (lift (S O) O x0) x2)
          end of h1
          (h2) 
             by (pr0_lift . . H1 . .)
             we proved pr0 (lift (S O) O v2) (lift (S O) O x0)
             by (pr0_comp . . previous . . H5 .)
             we proved 
                pr0
                  THead (Flat Appl) (lift (S O) O v2) t2
                  THead (Flat Appl) (lift (S O) O x0) x2
             by (pr0_comp . . H3 . . previous .)

                pr0
                  THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
                  THead (Bind b) x1 (THead (Flat Appl) (lift (S O) O x0) x2)
          end of h2
          by (ex_intro2 . . . . h1 h2)
          we proved 
             ex2
               T
               λt:T.pr0 (THead (Bind b) u1 (THead (Flat Appl) (lift (S O) O v1) t1)) t
               λt:T.pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) t
       we proved 
          ∀b:B
            .not (eq B b Abst)
              →∀v1:T
                   .∀v2:T
                     .∀x0:T
                       .pr0 v1 x0
                         →(pr0 v2 x0
                              →∀u1:T
                                   .∀u2:T
                                     .∀x1:T
                                       .pr0 u1 x1
                                         →(pr0 u2 x1
                                              →∀t1:T
                                                   .∀t2:T
                                                     .∀x2:T
                                                       .pr0 t1 x2
                                                         →(pr0 t2 x2
                                                              →(ex2
                                                                   T
                                                                   λt:T.pr0 (THead (Bind b) u1 (THead (Flat Appl) (lift (S O) O v1) t1)) t
                                                                   λt:T.pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) t))))