DEFINITION pr0_confluence__pr0_cong_upsilon_delta()
TYPE =
       not (eq B Abbr Abst)
         →∀u5:T
              .∀t2:T
                .∀w:T
                  .subst0 O u5 t2 w
                    →∀u2:T
                         .∀v2:T
                           .∀x:T
                             .pr0 u2 x
                               →(pr0 v2 x
                                    →∀t5:T
                                         .∀x0:T
                                           .pr0 t2 x0
                                             →(pr0 t5 x0
                                                  →∀u3:T
                                                       .∀x1:T
                                                         .pr0 u5 x1
                                                           →(pr0 u3 x1
                                                                →(ex2
                                                                     T
                                                                     λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                                                                     λt:T
                                                                       .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t))))
BODY =
        suppose H: not (eq B Abbr Abst)
        assume u5: T
        assume t2: T
        assume w: T
        suppose H0: subst0 O u5 t2 w
        assume u2: T
        assume v2: T
        assume x: T
        suppose H1: pr0 u2 x
        suppose H2: pr0 v2 x
        assume t5: T
        assume x0: T
        suppose H3: pr0 t2 x0
        suppose H4: pr0 t5 x0
        assume u3: T
        assume x1: T
        suppose H5: pr0 u5 x1
        suppose H6: pr0 u3 x1
          by (pr0_subst0 . . H3 . . . H0 . H5)
          we proved or (pr0 w x0) (ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x1 x0 w2)
          we proceed by induction on the previous result to prove 
             ex2
               T
               λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
               λt:T
                 .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
             case or_introl : H7:pr0 w x0 ⇒
                the thesis becomes 
                ex2
                  T
                  λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                  λt:T
                    .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
                   (h1) 
                      by (pr0_upsilon . H . . H1 . . H5 . . H7)

                         pr0
                           THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)
                           THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O x) x0)
                   end of h1
                   (h2) 
                      by (pr0_lift . . H2 . .)
                      we proved pr0 (lift (S O) O v2) (lift (S O) O x)
                      by (pr0_comp . . previous . . H4 .)
                      we proved 
                         pr0
                           THead (Flat Appl) (lift (S O) O v2) t5
                           THead (Flat Appl) (lift (S O) O x) x0
                      by (pr0_comp . . H6 . . previous .)

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

                      ex2
                        T
                        λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                        λt:T
                          .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
             case or_intror : H7:ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x1 x0 w2 ⇒
                the thesis becomes 
                ex2
                  T
                  λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                  λt:T
                    .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
                   we proceed by induction on H7 to prove 
                      ex2
                        T
                        λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                        λt:T
                          .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
                      case ex_intro2 : x2:T H8:pr0 w x2 H9:subst0 O x1 x0 x2 ⇒
                         the thesis becomes 
                         ex2
                           T
                           λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                           λt:T
                             .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
                            (h1) 
                               by (pr0_upsilon . H . . H1 . . H5 . . H8)

                                  pr0
                                    THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)
                                    THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O x) x2)
                            end of h1
                            (h2) 
                               (h1) 
                                  by (pr0_lift . . H2 . .)
                                  we proved pr0 (lift (S O) O v2) (lift (S O) O x)
                                  by (pr0_comp . . previous . . H4 .)

                                     pr0
                                       THead (Flat Appl) (lift (S O) O v2) t5
                                       THead (Flat Appl) (lift (S O) O x) x0
                               end of h1
                               (h2) 
                                  consider H9
                                  we proved subst0 O x1 x0 x2
                                  that is equivalent to subst0 (s (Flat Appl) O) x1 x0 x2
                                  by (subst0_snd . . . . . previous .)

                                     subst0
                                       O
                                       x1
                                       THead (Flat Appl) (lift (S O) O x) x0
                                       THead (Flat Appl) (lift (S O) O x) x2
                               end of h2
                               by (pr0_delta . . H6 . . h1 . h2)

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

                               ex2
                                 T
                                 λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                                 λt:T
                                   .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t

                      ex2
                        T
                        λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                        λt:T
                          .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
          we proved 
             ex2
               T
               λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
               λt:T
                 .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t
       we proved 
          not (eq B Abbr Abst)
            →∀u5:T
                 .∀t2:T
                   .∀w:T
                     .subst0 O u5 t2 w
                       →∀u2:T
                            .∀v2:T
                              .∀x:T
                                .pr0 u2 x
                                  →(pr0 v2 x
                                       →∀t5:T
                                            .∀x0:T
                                              .pr0 t2 x0
                                                →(pr0 t5 x0
                                                     →∀u3:T
                                                          .∀x1:T
                                                            .pr0 u5 x1
                                                              →(pr0 u3 x1
                                                                   →(ex2
                                                                        T
                                                                        λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t
                                                                        λt:T
                                                                          .pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t))))