DEFINITION pr2_delta1()
TYPE =
       ∀c:C
         .∀d:C
           .∀u:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) u)
                 →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t:T.(subst1 i u t2 t)→(pr2 c t1 t)
BODY =
Show proof