DEFINITION pr2_confluence__pr2_free_delta()
TYPE =
       ∀c:C
         .∀d:C
           .∀t0:T
             .∀t1:T
               .∀t2:T
                 .∀t4:T
                   .∀u:T
                     .∀i:nat
                       .pr0 t0 t1
                         →(getl i c (CHead d (Bind Abbr) u)
                              →(pr0 t0 t4)→(subst0 i u t4 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t))
BODY =
Show proof