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