DEFINITION pr0_confluence__pr0_upsilon_upsilon()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀v1:T
                .∀v2:T
                  .∀x0:T
                    .pr0 v1 x0
                      →(pr0 v2 x0
                           →∀u1:T
                                .∀u2:T
                                  .∀x1:T
                                    .pr0 u1 x1
                                      →(pr0 u2 x1
                                           →∀t1:T
                                                .∀t2:T
                                                  .∀x2:T
                                                    .pr0 t1 x2
                                                      →(pr0 t2 x2
                                                           →(ex2
                                                                T
                                                                λt:T.pr0 (THead (Bind b) u1 (THead (Flat Appl) (lift (S O) O v1) t1)) t
                                                                λt:T.pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) t))))
BODY =
Show proof