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