DEFINITION pr0_confluence__pr0_delta_tau()
TYPE =
       ∀u2:T
         .∀t3:T
           .∀w:T
             .subst0 O u2 t3 w
               →∀t4:T
                    .pr0 (lift (S O) O t4) t3
                      →∀t2:T.(ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t)
BODY =
Show proof