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