DEFINITION pr2_ind()
TYPE =
       ∀P:C→T→T→Prop
         .∀c:C.∀t:T.∀t1:T.(pr0 t t1)→(P c t t1)
           →(∀c:C
                  .∀c1:C
                    .∀t:T
                      .∀n:nat
                        .getl n c (CHead c1 (Bind Abbr) t)
                          →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t3:T.(subst0 n t t2 t3)→(P c t1 t3)
                →∀c:C.∀t:T.∀t1:T.(pr2 c t t1)→(P c t t1))
BODY =
Show proof