DEFINITION pr0_confluence__pr0_cong_delta()
TYPE =
       ∀u3:T
         .∀t5:T
           .∀w:T
             .subst0 O u3 t5 w
               →∀u2:T
                    .∀x:T
                      .pr0 u2 x
                        →(pr0 u3 x
                             →∀t3:T
                                  .∀x0:T
                                    .pr0 t3 x0
                                      →(pr0 t5 x0
                                           →ex2 T λt:T.pr0 (THead (Bind Abbr) u2 t3) t λt:T.pr0 (THead (Bind Abbr) u3 w) t))
BODY =
Show proof