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 =
Show proof