DEFINITION pr0_confluence__pr0_cong_upsilon_cong()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀u2:T
                .∀v2:T
                  .∀x:T
                    .pr0 u2 x
                      →(pr0 v2 x
                           →∀t2:T
                                .∀t5:T
                                  .∀x0:T
                                    .pr0 t2 x0
                                      →(pr0 t5 x0
                                           →∀u5:T
                                                .∀u3:T
                                                  .∀x1:T
                                                    .pr0 u5 x1
                                                      →(pr0 u3 x1
                                                           →(ex2
                                                                T
                                                                λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind b) u5 t2)) t
                                                                λt:T.pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t))))
BODY =
        assume b: B
        suppose H: not (eq B b Abst)
        assume u2: T
        assume v2: T
        assume x: T
        suppose H0: pr0 u2 x
        suppose H1: pr0 v2 x
        assume t2: T
        assume t5: T
        assume x0: T
        suppose H2: pr0 t2 x0
        suppose H3: pr0 t5 x0
        assume u5: T
        assume u3: T
        assume x1: T
        suppose H4: pr0 u5 x1
        suppose H5: pr0 u3 x1
          (h1) 
             by (pr0_upsilon . H . . H0 . . H4 . . H2)

                pr0
                  THead (Flat Appl) u2 (THead (Bind b) u5 t2)
                  THead (Bind b) x1 (THead (Flat Appl) (lift (S O) O x) x0)
          end of h1
          (h2) 
             by (pr0_lift . . H1 . .)
             we proved pr0 (lift (S O) O v2) (lift (S O) O x)
             by (pr0_comp . . previous . . H3 .)
             we proved 
                pr0
                  THead (Flat Appl) (lift (S O) O v2) t5
                  THead (Flat Appl) (lift (S O) O x) x0
             by (pr0_comp . . H5 . . previous .)

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