DEFINITION pr0_confluence__pr0_cong_delta()
TYPE =
       ∀u3:T
         .∀t5:T
           .∀w:T
             .subst0 O u3 t5 w
               →∀u2:T
                    .∀x:T
                      .pr0 u2 x
                        →(pr0 u3 x
                             →∀t3:T
                                  .∀x0:T
                                    .pr0 t3 x0
                                      →(pr0 t5 x0
                                           →ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t))
BODY =
        assume u3: T
        assume t5: T
        assume w: T
        suppose H: subst0 O u3 t5 w
        assume u2: T
        assume x: T
        suppose H0: pr0 u2 x
        suppose H1: pr0 u3 x
        assume t3: T
        assume x0: T
        suppose H2: pr0 t3 x0
        suppose H3: pr0 t5 x0
          by (pr0_subst0 . . H3 . . . H . H1)
          we proved or (pr0 w x0) (ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2)
          we proceed by induction on the previous result to prove 
             ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
             case or_introl : H4:pr0 w x0 ⇒
                the thesis becomes 
                ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
                   (h1) 
                      by (pr0_comp . . H0 . . H2 .)
pr0 (THead (Bind Abbr) u2 t3) (THead (Bind Abbr) x x0)
                   end of h1
                   (h2) 
                      by (pr0_comp . . H1 . . H4 .)
pr0 (THead (Bind Abbr) u3 w) (THead (Bind Abbr) x x0)
                   end of h2
                   by (ex_intro2 . . . . h1 h2)

                      ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
             case or_intror : H4:ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2 ⇒
                the thesis becomes 
                ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
                   we proceed by induction on H4 to prove 
                      ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
                      case ex_intro2 : x1:T H5:pr0 w x1 H6:subst0 O x x0 x1 ⇒
                         the thesis becomes 
                         ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
                            (h1) 
                               by (pr0_delta . . H0 . . H2 . H6)
pr0 (THead (Bind Abbr) u2 t3) (THead (Bind Abbr) x x1)
                            end of h1
                            (h2) 
                               by (pr0_comp . . H1 . . H5 .)
pr0 (THead (Bind Abbr) u3 w) (THead (Bind Abbr) x x1)
                            end of h2
                            by (ex_intro2 . . . . h1 h2)

                               ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t

                      ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
          we proved 
             ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t
       we proved 
          ∀u3:T
            .∀t5:T
              .∀w:T
                .subst0 O u3 t5 w
                  →∀u2:T
                       .∀x:T
                         .pr0 u2 x
                           →(pr0 u3 x
                                →∀t3:T
                                     .∀x0:T
                                       .pr0 t3 x0
                                         →(pr0 t5 x0
                                              →ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t))