DEFINITION pr0_confluence__pr0_cong_upsilon_refl()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀u0:T
                .∀u3:T
                  .pr0 u0 u3
                    →∀t4:T
                         .∀t5:T
                           .pr0 t4 t5
                             →∀u2:T
                                  .∀v2:T
                                    .∀x:T
                                      .pr0 u2 x
                                        →(pr0 v2 x
                                             →(ex2
                                                  T
                                                  λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind b) u0 t4)) 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 u0: T
        assume u3: T
        suppose H0: pr0 u0 u3
        assume t4: T
        assume t5: T
        suppose H1: pr0 t4 t5
        assume u2: T
        assume v2: T
        assume x: T
        suppose H2: pr0 u2 x
        suppose H3: pr0 v2 x
          (h1) 
             by (pr0_upsilon . H . . H2 . . H0 . . H1)

                pr0
                  THead (Flat Appl) u2 (THead (Bind b) u0 t4)
                  THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O x) t5)
          end of h1
          (h2) 
             (h1) by (pr0_refl .) we proved pr0 u3 u3
             (h2) 
                (h1) 
                   by (pr0_lift . . H3 . .)
pr0 (lift (S O) O v2) (lift (S O) O x)
                end of h1
                (h2) by (pr0_refl .) we proved pr0 t5 t5
                by (pr0_comp . . h1 . . h2 .)

                   pr0
                     THead (Flat Appl) (lift (S O) O v2) t5
                     THead (Flat Appl) (lift (S O) O x) t5
             end of h2
             by (pr0_comp . . h1 . . h2 .)

                pr0
                  THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t5)
                  THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O x) t5)
          end of h2
          by (ex_intro2 . . . . h1 h2)
          we proved 
             ex2
               T
               λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind b) u0 t4)) 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)
              →∀u0:T
                   .∀u3:T
                     .pr0 u0 u3
                       →∀t4:T
                            .∀t5:T
                              .pr0 t4 t5
                                →∀u2:T
                                     .∀v2:T
                                       .∀x:T
                                         .pr0 u2 x
                                           →(pr0 v2 x
                                                →(ex2
                                                     T
                                                     λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind b) u0 t4)) t
                                                     λt:T.pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t))