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