DEFINITION pr0_confluence__pr0_cong_upsilon_cong()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀u2:T
                .∀v2:T
                  .∀x:T
                    .pr0 u2 x
                      →(pr0 v2 x
                           →∀t2:T
                                .∀t5:T
                                  .∀x0:T
                                    .pr0 t2 x0
                                      →(pr0 t5 x0
                                           →∀u5:T
                                                .∀u3:T
                                                  .∀x1:T
                                                    .pr0 u5 x1
                                                      →(pr0 u3 x1
                                                           →(ex2
                                                                T
                                                                λt:T.pr0 (THead (Flat Appl) u2 (THead (Bind b) u5 t2)) t
                                                                λt:T.pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t5)) t))))
BODY =
Show proof