DEFINITION pr0_confluence__pr0_cong_upsilon_zeta()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀u0:T
                .∀u3:T
                  .pr0 u0 u3
                    →∀u2:T
                         .∀v2:T
                           .∀x0:T
                             .pr0 u2 x0
                               →(pr0 v2 x0
                                    →∀x:T
                                         .∀t3:T
                                           .∀x1:T
                                             .pr0 x x1
                                               →(pr0 t3 x1
                                                    →(ex2
                                                         T
                                                         λt:T.pr0 (THead (Flat Appl) u2 t3) t
                                                         λt:T
                                                           .pr0
                                                             THead
                                                               Bind b
                                                               u3
                                                               THead (Flat Appl) (lift (S O) O v2) (lift (S O) O x)
                                                             t)))
BODY =
        assume b: B
        suppose H: not (eq B b Abst)
        assume u0: T
        assume u3: T
        suppose : pr0 u0 u3
        assume u2: T
        assume v2: T
        assume x0: T
        suppose H1: pr0 u2 x0
        suppose H2: pr0 v2 x0
        assume x: T
        assume t3: T
        assume x1: T
        suppose H3: pr0 x x1
        suppose H4: pr0 t3 x1
          by (lift_flat . . . . .)
          we proved 
             eq
               T
               lift (S O) O (THead (Flat Appl) v2 x)
               THead (Flat Appl) (lift (S O) O v2) (lift (S O) O x)
          we proceed by induction on the previous result to prove 
             ex2
               T
               λt0:T.pr0 (THead (Flat Appl) u2 t3) t0
               λt0:T
                 .pr0
                   THead
                     Bind b
                     u3
                     THead (Flat Appl) (lift (S O) O v2) (lift (S O) O x)
                   t0
             case refl_equal : ⇒
                the thesis becomes 
                ex2
                  T
                  λt:T.pr0 (THead (Flat Appl) u2 t3) t
                  λt:T.pr0 (THead (Bind b) u3 (lift (S O) O (THead (Flat Appl) v2 x))) t
                   (h1) 
                      by (pr0_comp . . H1 . . H4 .)
pr0 (THead (Flat Appl) u2 t3) (THead (Flat Appl) x0 x1)
                   end of h1
                   (h2) 
                      by (pr0_comp . . H2 . . H3 .)
                      we proved pr0 (THead (Flat Appl) v2 x) (THead (Flat Appl) x0 x1)
                      by (pr0_zeta . H . . previous .)

                         pr0
                           THead (Bind b) u3 (lift (S O) O (THead (Flat Appl) v2 x))
                           THead (Flat Appl) x0 x1
                   end of h2
                   by (ex_intro2 . . . . h1 h2)

                      ex2
                        T
                        λt:T.pr0 (THead (Flat Appl) u2 t3) t
                        λt:T.pr0 (THead (Bind b) u3 (lift (S O) O (THead (Flat Appl) v2 x))) t
          we proved 
             ex2
               T
               λt0:T.pr0 (THead (Flat Appl) u2 t3) t0
               λt0:T
                 .pr0
                   THead
                     Bind b
                     u3
                     THead (Flat Appl) (lift (S O) O v2) (lift (S O) O x)
                   t0
       we proved 
          ∀b:B
            .not (eq B b Abst)
              →∀u0:T
                   .∀u3:T
                     .pr0 u0 u3
                       →∀u2:T
                            .∀v2:T
                              .∀x0:T
                                .pr0 u2 x0
                                  →(pr0 v2 x0
                                       →∀x:T
                                            .∀t3:T
                                              .∀x1:T
                                                .pr0 x x1
                                                  →(pr0 t3 x1
                                                       →(ex2
                                                            T
                                                            λt0:T.pr0 (THead (Flat Appl) u2 t3) t0
                                                            λt0:T
                                                              .pr0
                                                                THead
                                                                  Bind b
                                                                  u3
                                                                  THead (Flat Appl) (lift (S O) O v2) (lift (S O) O x)
                                                                t0)))